diff options
| author | notin | 2012-12-13 10:19:48 +0000 |
|---|---|---|
| committer | Pierre Letouzey | 2014-12-09 12:14:39 +0100 |
| commit | feeacd6e4a805e5d288b97132a02011afaba5e7f (patch) | |
| tree | c391d33f58fea1fec269c05ed15fdc4227cdc86d /tools | |
| parent | f8cb1942284979bc7c325f2137fad1293380d855 (diff) | |
Port to trunk commit r16062 of v8.4 (Correction des entĂȘtes pour la documentation en ligne)
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 |
