diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/output.ml | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 67a28bfd7c..a3e4c4000f 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -543,10 +543,7 @@ module Html = struct end let trailer () = - if !index && (get_module false) <> "Index" then - printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; - if !header_trailer then - if !footer_file_spec then + if !header_trailer && !footer_file_spec then let cin = Pervasives.open_in !footer_file in try while true do @@ -554,12 +551,14 @@ module Html = struct printf "%s\n" s done with End_of_file -> Pervasives.close_in cin - else - begin - printf "<hr/>This page has been generated by "; - printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq; - printf "</div>\n\n</div>\n\n</body>\n</html>" - end + else + begin + if !index && (get_module false) <> "Index" then + printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; + printf "<hr/>This page has been generated by "; + printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq; + printf "</div>\n\n</div>\n\n</body>\n</html>" + end let start_module () = let ln = !lib_name in |