diff options
| -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 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 |