$title" . (strlen($title2) ? ": " . htmlspecialchars($title2) : "") . "
\n"; if ($_SESSION["messages"]) { echo " \n \n"; $_SESSION["messages"] = array(); } $databases = &$_SESSION["databases"][$_GET["server"]]; if (strlen($_GET["db"]) && $databases && !in_array($_GET["db"], $databases, true)) { $databases = null; } if (isset($databases) && !isset($_GET["sql"]) && !isset($_SESSION["coverage"])) { // improves concurrency if a user opens several pages at once session_write_close(); } if ($error) { echo "$error
\n";
}
}
function page_footer($missing = false) {
global $SELF, $VERSION, $dbh;
?>