... if (!isset($PAGE_TITLE)) { http_response_code(500); die("\$PAGE_TITLE not set"); } echo "
E949: $PAGE_TITLE
\n"; require_once("favicon.html"); ?>