diff options
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index c16e2751bc..910c81381b 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -350,7 +350,7 @@ let rec loop doc = not possible due exceptions. *) in vernac_loop doc (Stm.get_current_state ~doc) with - | CErrors.Drop -> () + | CErrors.Drop -> doc | CErrors.Quit -> exit 0 | any -> Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++ |