From ceee412ccf9dcfe85c97a1f5c6b684af04b697f2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 23 Jul 2008 14:46:57 +0000
Subject: Stop glob messages to be printed by default on stdout

Jean-Marc, feel free to check I've not broken anything concerning coqdoc...



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11248 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/dumpglob.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 175a149431..a8f4b31d2d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -21,9 +21,6 @@ let open_glob_file f =
 let close_glob_file () =
   Pervasives.close_out !glob_file
 
-let dump_string s = 
-  Pervasives.output_string !glob_file s
-
 type glob_output_t = 
     | NoGlob
     | StdOut
@@ -44,6 +41,9 @@ let dump_to_dotglob f = glob_output := MultFiles
 
 let dump_into_file f = glob_output := File f; open_glob_file f
 
+let dump_string s = 
+  if dump () then Pervasives.output_string !glob_file s
+
 
 let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output; glob_output := NoGlob
-- 
cgit v1.2.3