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')
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 7b7ebd1dc..586a20875 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