\n";
/* remove other path prefixes than /manual/ */
$legal_paths = array("/manual" => 1);
$tmp = strrchr($page_url, "/");
if ($tmp) {
$path = substr($page_url, 0, strlen($page_url)-strlen($tmp));
if ($legal_paths[$path]) {
$page_name = "$DOCUMENT_ROOT/" . ereg_replace("^/", "", $page_url);
} else {
$page_name = substr($tmp, 1, strlen($tmp));
}
} else {
$page_name = $page_url;
}
echo "\n";
show_source($page_name);
commonFooter();
?>