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) --- doc/common/styles/html/coqremote/footer.html | 69 ++++++++++++---------------- doc/common/styles/html/coqremote/header.html | 60 +++++++++++------------- tools/coqdoc/output.ml | 19 ++++---- 3 files changed, 66 insertions(+), 82 deletions(-) diff --git a/doc/common/styles/html/coqremote/footer.html b/doc/common/styles/html/coqremote/footer.html index 138c30253f..ff38ba8a32 100644 --- a/doc/common/styles/html/coqremote/footer.html +++ b/doc/common/styles/html/coqremote/footer.html @@ -1,45 +1,34 @@ -
- -
- - - - - - - +
+ +
+ + + + - diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html index afcdbe73af..891fb32808 100644 --- a/doc/common/styles/html/coqremote/header.html +++ b/doc/common/styles/html/coqremote/header.html @@ -6,44 +6,40 @@ Standard Library | The Coq Proof Assistant - + - - - + + + - - + +
-
- -
- - - -
+ + + + +
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 "
\n\n
\n
Index" !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 "
This page has been generated by "; - printf "coqdoc\n" Coq_config.wwwcoq; - printf "
\n\n
\n\n\n" - end + else + begin + if !index && (get_module false) <> "Index" then + printf "
\n\n
\n
Index" !index_name; + printf "
This page has been generated by "; + printf "coqdoc\n" Coq_config.wwwcoq; + printf "
\n\n\n\n\n" + end let start_module () = let ln = !lib_name in -- cgit v1.2.3