");
define("TITLE_COLOR", " bgcolor=000000 ");
define("TITLE_FONT", " ");
define("BODY_COLOR", " bgcolor=ffffff ");
define("NOLOGIN", "Not logged in. Click here to login.\n");
function boinc_real_escape_string($unstripped) {
if (1) {
// valid for PHP>=4.3.0, 5. If there is a run-time php_version() function please use it
// instead of this hack!
return mysql_real_escape_string($unstripped);
} else {
return str_replace("\'", "'", str_replace("\\\"", "'", $unstripped));
}
}
function admin_page_head($title) {
echo "$title\n";
echo TABLE . "