From a85cf9c7eb64d15955d4998efed6b52d91381bfd Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 7 Apr 2004 12:25:34 +0000
Subject: Coqdoc backtrack: HTML special characters are no longer quoted inside
 # ... #; ^ ... ^ special verbatim code also backtracked.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5651 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/xmlcommand.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/xml/xmlcommand.ml')

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index feaf1b8087..38c270db5a 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -430,7 +430,7 @@ let theory_buffer = Buffer.create 4000;;
 
 let theory_output_string ?(do_not_quote = false) s = 
   (* prepare for coqdoc post-processing *)
-  let s = if do_not_quote then s else "(** ^"^s^"\n^*)\n" in
+  let s = if do_not_quote then s else "(** #"^s^"\n#*)\n" in
   print_if_verbose s;
    Buffer.add_string theory_buffer s
 ;;
-- 
cgit v1.2.3