aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--toplevel/coqtop.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a486de2e2..779cd06bf 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -351,6 +351,8 @@ let init arglist =
flush_all();
if not !batch_mode then
fatal_error (str "Error during initialization:" ++ fnl () ++ Toplevel.print_toplevel_error e)
+ else
+ fatal_error (Toplevel.print_toplevel_error e)
end;
if !batch_mode then
(flush_all();