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 +++---
 toplevel/vernac.ml | 3 +--
 2 files changed, 4 insertions(+), 5 deletions(-)

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
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ae35b0fa1a..92d2bbf28b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -228,8 +228,7 @@ let compile verbosely f =
   let ldir,long_f_dot_v = Library.start_library f in
     if Dumpglob.multi_dump () then 
       Dumpglob.open_glob_file (f ^ ".glob");
-    if Dumpglob.dump () then
-      Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
+    Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
     if !Flags.xml_export then !xml_start_library ();
     let _ = load_vernac verbosely long_f_dot_v in
      if Pfedit.get_all_proof_names () <> [] then
-- 
cgit v1.2.3