From e1d32b26956ca7bb5e568fd7e0b615d59df44e49 Mon Sep 17 00:00:00 2001 From: sacerdot Date: Thu, 8 Jul 2004 17:08:11 +0000 Subject: * tag no longer generated for theory files (the HELM/MoWGLI stylesheets do not longer require it) * helm:helm_link added to each element whose href is an URI * the required element was not generated for theories git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5877 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/xml/xmlcommand.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'contrib/xml/xmlcommand.ml') diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 7b7ebd1dcc..586a208755 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -644,14 +644,14 @@ let _ = "%xhtml-special.ent;\n" ^ "%xhtml-symbol.ent;\n" ^ "]>\n\n"); - theory_output_string "\n"; - theory_output_string "\n\n\n") + theory_output_string "\n"; + theory_output_string "\n\n") ;; let _ = Vernac.set_xml_end_library (function () -> - theory_output_string "\n"; + theory_output_string "\n\n"; let ofn = theory_filename xml_library_root in begin match ofn with @@ -701,6 +701,6 @@ let _ = let _ = Library.set_xml_require (fun d -> theory_output_string - (Printf.sprintf "Require %s.
" + (Printf.sprintf "Require %s.
" (uri_of_dirpath d) (Names.string_of_dirpath d))) ;; -- cgit v1.2.3