aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 5521e8a40..2cb608326 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -13,7 +13,9 @@ open Flags
open Vernac
open Pcoq
-let top_stderr x = msg_with ~pp_tag:Ppstyle.to_format !Pp_control.err_ft x
+let top_stderr x =
+ pp_with ~pp_tag:Ppstyle.to_format !Pp_control.err_ft x;
+ Format.pp_print_flush !Pp_control.err_ft ()
(* A buffer for the character read from a channel. We store the command
* entered to be able to report errors without pretty-printing. *)