From b86ca3fec598d4bd50424adef5b5fd09877bee26 Mon Sep 17 00:00:00 2001
From: Gabor Hojtsy <goba@php.net>
Date: Fri, 8 Aug 2003 13:35:25 +0000
Subject: [PATCH] The manual path does not need to end in /manual/ :)

---
 source.php | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/source.php b/source.php
index 2f2605567..971b4efbe 100644
--- a/source.php
+++ b/source.php
@@ -61,7 +61,7 @@ if (!empty($dir) && !preg_match("!^(\\.|/)$!", $dir)) {
         "/error"   => 1,
         "/license" => 1
     );
-    if (preg_match("!^/manual/$!", $dir) || isset($legal_dirs[$dir])) {
+    if (preg_match("!^/manual/!", $dir) || isset($legal_dirs[$dir])) {
         $page_name = $_SERVER['DOCUMENT_ROOT'] . $_GET['url'];
     } else { $page_name = FALSE; }
 } else {