From feeacd6e4a805e5d288b97132a02011afaba5e7f Mon Sep 17 00:00:00 2001
From: notin
Date: Thu, 13 Dec 2012 10:19:48 +0000
Subject: Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la
 documentation en ligne)

---
 tools/coqdoc/output.ml | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

(limited to 'tools')

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
-- 
cgit v1.2.3