From 76d6be7020f89b25de0c06e88487700ee77b1881 Mon Sep 17 00:00:00 2001
From: moodler <moodler>
Date: Sun, 10 Nov 2002 14:05:52 +0000
Subject: [PATCH] Put a menu on the documentation

---
 doc/top.php | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/top.php b/doc/top.php
index 65eae35720..4f58d44048 100644
--- a/doc/top.php
+++ b/doc/top.php
@@ -6,7 +6,7 @@
         error("Site is misconfigured");
     }
     $strdocumentation = get_string("documentation");
-    print_header("$site->shortname: $strdocumentation", "$site->fullname", "$strdocumentation");
+    print_header("$site->shortname: $strdocumentation", "$site->fullname", "$strdocumentation", "", "", true, "", navmenu($site));
     
 ?>
 
-- 
2.39.5