From 3a485ed0feaccf629772494a3806881e168980d6 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 14 Mar 2013 16:22:43 +0000
Subject: Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)

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

(limited to 'toplevel/vernac.ml')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f46ef8f13..faf4f1bdd 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -240,7 +240,7 @@ let pr_new_syntax loc ocom =
     | Some com -> Ppvernac.pr_vernac com
     | None -> mt() in
   if !beautify_file then
-    pp (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
+    msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
     msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
-- 
cgit v1.2.3