// +---------------------------------------------------------------------- // $Id$ if (is_file($_SERVER["DOCUMENT_ROOT"] . $_SERVER["REQUEST_URI"])) { return false; } else { if (!isset($_SERVER['PATH_INFO'])) { $_SERVER['PATH_INFO'] = $_SERVER['REQUEST_URI']; } require __DIR__ . "/index.php"; }