From cb615fd741353dde4a562e1b4098c9e622b93f32 Mon Sep 17 00:00:00 2001
From: notin
Date: Mon, 21 Jul 2008 14:29:13 +0000
Subject: Suite commit 11236

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

(limited to 'interp')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index b8121af866..ca817b776b 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -25,23 +25,26 @@ let dump_string s =
   Pervasives.output_string !glob_file s
 
 type glob_output_t = 
-    | None
+    | NoGlob
     | StdOut
     | MultFiles
     | File of string
 
-let glob_output = ref MultFiles
+let glob_output = ref NoGlob
 
-let dump () = !glob_output != None
+let dump () = !glob_output != NoGlob
 
-let noglob () = glob_output := None
+let noglob () = glob_output := NoGlob
 
-let dump_to_stdout () = glob_output := StdOut
+let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
 
 let multi_dump () = !glob_output = MultFiles
 
+let dump_to_dotglob f = glob_output := MultFiles
+
 let dump_into_file f = glob_output := File f; open_glob_file f
 
+
 let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output
 let continue () = glob_output := !previous_state
-- 
cgit v1.2.3