diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-23 13:45:42 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-23 13:45:42 +0000 |
| commit | 75cc98ac3de600d872eba7891852f8bb121f151b (patch) | |
| tree | 1af25fc74a2e596656294e5e30f72005ccdcb8c1 /toplevel | |
| parent | df9ef93cd565a7a45589dd77ba8aa1a2ab81dcec (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 76e9c2fef..53b3f5893 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 |