diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-22 16:46:05 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-22 16:46:05 +0000 |
commit | d672ce42ecd1fd6845f1c9ea178f5d9fd05afb2c (patch) | |
tree | 4fa2dae3c0542a6d9fa9e607bf4d97bfb4f87b78 /tools/coqdoc/output.ml | |
parent | 1d6a9cd4ac13b69d1aa5b06f7046685f2fe400ba (diff) |
Corrections des bugs #1730 et #1731
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10246 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/output.ml')
-rw-r--r-- | tools/coqdoc/output.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 45017db8d..9b823bca8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -289,8 +289,8 @@ module Html = struct if !index && !current_module <> "Index" then printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>"; if !header_trailer then begin - printf "<hr/><font size=\"-1\">This page has been generated by "; - printf "<a href=\"%s\">coqdoc</a></font>\n" self; + printf "<hr/>This page has been generated by "; + printf "<a href=\"%s\">coqdoc</a>\n" self; printf "</div>\n\n</div>\n\n</body>\n</html>" end @@ -424,9 +424,9 @@ module Html = struct let r = sprintf "%s.html#%s" !current_module lab in add_toc_entry (Toc_section (lev, f, r)); stop_item (); - printf "<a name=\"%s\"></a><h%d>" lab lev; + printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev; f (); - printf "</h%d class=\"section\">\n" lev + printf "</h%d>\n" lev let rule () = printf "<hr/>\n" |