From a5b11b8007f55c7d9b606410b69950e54309de26 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 10 Sep 2003 09:24:30 +0000
Subject: Oubli des guillemets dans Comments

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

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 100ac9d6ca..d8d3493163 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -151,7 +151,7 @@ let pr_production_item = function
 
 let pr_comment pr_c = function
   | CommentConstr c -> pr_c c
-  | CommentString s -> str s
+  | CommentString s -> qs s
   | CommentInt n -> int n
 
 let pr_in_out_modules = function
-- 
cgit v1.2.3