• URL/server_status.php: human-readable (web page).
  • URL/server_status.php?xml=1: XML format, as follows: ".html_text(" 1127772607 jocelyn BOINC database running castelli master science database running kryten sah_validate4 running ... 563389 1198237 19 16 0 0 -0.0002777 ")."

    There are two ways to do this:

    1. Copy the file server_status.php from html/ops to html/user. This works fine as long as you don't need any customization, and the DB queries in the page only take a few seconds (the page is cached, so they are done infrequently).
    2. Write a periodic script that generates the 2 pages as files, and put a script in user/server_status.php that echoes one file or the other.
    "; page_tail(); ?>