aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authornotin2012-12-13 10:19:48 +0000
committerPierre Letouzey2014-12-09 12:14:39 +0100
commitfeeacd6e4a805e5d288b97132a02011afaba5e7f (patch)
treec391d33f58fea1fec269c05ed15fdc4227cdc86d /tools
parentf8cb1942284979bc7c325f2137fad1293380d855 (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.ml19
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