Put a menu on the documentation

diff --git a/doc/top.php b/doc/top.php
index 65eae3572067d4991cbb5bfd623ce72d2d82341a..4f58d44048f82cd4c3a5ecf05f30281b1d4e2757 100644 (file)
--- 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));
     
 ?>