End the page with correct HTML.

diff --git a/doc/contents.php b/doc/contents.php
index dba83a7d43919930718c7c2685d8a2d0ba3a13da..243b520103968b09d7775f6c77fa0a1dcecfd71e 100755 (executable)
--- a/doc/contents.php
+++ b/doc/contents.php
@@ -32,5 +32,7 @@
         echo '</ul>';
     }
 
+    // Sloppy way to produce valid markup... there should be a print_footer_minimal().
+    echo '</div></div></body></html>';
     \r
 ?>\r