Slightly more rboust

diff --git a/doc/index.php b/doc/index.php
index 1e4d03b4704c92a148aae5219071c6a0b7c0d695..66b6f81290d089c1b66c8db70c4d5290d6d82d0f 100644 (file)
--- a/doc/index.php
+++ b/doc/index.php
@@ -14,6 +14,8 @@
 
     if (!empty($sub)) {
         $sub = "#$sub";
+    } else {
+        $sub = "";
     }
 
     if (empty($file)) {