diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-10 08:50:16 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-10 08:50:16 +0200 |
| commit | 7b32d8454ded5497d677d5dbcc665aacb6725e6b (patch) | |
| tree | cc0c2c76eda49943edd452cffd3e0d9de3606bb7 /toplevel | |
| parent | f3f387e63789def93219f407bb2a35257143b73d (diff) | |
| parent | e95b816ed34a379e6b6f38630e416710d66c4179 (diff) | |
Merge PR#547: [toplevel] Remove the feedback printer only on exit.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4968804fd..aca94e63d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -92,11 +92,11 @@ let console_toploop_run () = Dumpglob.noglob () end; Coqloop.loop(); - (* We remove the feeder but it could be ok not to do so *) - Feedback.del_feeder tl_feed; (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); - Mltop.ocaml_toploop() + Mltop.ocaml_toploop(); + (* We let the feeder in place for users of Drop *) + Feedback.del_feeder tl_feed let toploop_run = ref console_toploop_run |