Put a menu on the documentation

diff --git a/doc/top.php b/doc/top.php
index 65eae35..4f58d44 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));
     
 ?>