From 75cc98ac3de600d872eba7891852f8bb121f151b Mon Sep 17 00:00:00 2001
From: pboutill
Date: Mon, 23 Jan 2012 13:45:42 +0000
Subject: Bug 739: forbid dumpglob while using Coqtop in interactive mode

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14935 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/coqtop.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 76e9c2fef6..53b3f58933 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -354,7 +354,12 @@ let init arglist =
 let init_toplevel = init
 
 let start () =
-  init_toplevel (List.tl (Array.to_list Sys.argv));
+  let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
+  (* In batch mode, Coqtop has already exited at this point. In interactive one,
+     dump glob is nothing but garbage ...  *)
+  let () = if Dumpglob.dump () then
+    let () = if_verbose warning "Dumpglob cannot be used in interactive mode." in
+    Dumpglob.noglob () in
   if !ide_slave then
     Ide_slave.loop ()
   else
-- 
cgit v1.2.3