From 58fc89afc59941f825088974b0e7aaf5d4df571a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 18 Nov 2003 11:14:00 +0000
Subject: Bug: faut brancher la sortie des tactiques sur stdout pendant
 traduction

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

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ff674bc0bf..7aae0f38d4 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -136,11 +136,12 @@ let post_printing loc (env,t,f,n) = function
   | VernacSolve (i,_,deftac) ->
       set_formatter_translator();
       let pp = Ppvernacnew.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in
-      if !translate_file then begin
+      (if !translate_file then begin
 	msg (hov 0 (comment (fst loc) ++ pp ++ comment (snd loc - 1)));
       end
       else
-	msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pp))
+	msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pp)));
+      Format.set_formatter_out_channel stdout
   | _ -> ()
 
 let pr_new_syntax loc ocom =
-- 
cgit v1.2.3