From e95b816ed34a379e6b6f38630e416710d66c4179 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 7 Apr 2017 16:02:16 +0200
Subject: [toplevel] Remove the feedback feeder printing only on exit.

This fixes the bug in `Drop` reported by @mattam82: after performing a
`Drop`, the feeder was lost and no further message from Coq was
printed.
---
 toplevel/coqtop.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 4968804fde..aca94e63d2 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
 
-- 
cgit v1.2.3