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
---
 toplevel/vernac.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'toplevel')

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