document.title='".htmlspecialchars($current_page_title)."';\n"; }