diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-10 03:22:24 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-10 03:22:24 +0200 |
commit | b89c8f3846e8254651dbcba262f83d3d1fe3adb6 (patch) | |
tree | 637106259894dc99ae71a5e1edb938ba5dfc7f62 /toplevel | |
parent | dffba98368b5b1156e1933dc7377317281c57491 (diff) |
[toplevel] Print error header on fatal batch error.
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a61ade784..f0c77875a 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -111,7 +111,7 @@ let pr_open_cur_subgoals () = with Proof_global.NoCurrentProof -> Pp.str "" let vernac_error msg = - Format.fprintf !Topfmt.err_ft "@[%a@]%!" Pp.pp_with msg; + Topfmt.std_logger Feedback.Error msg; flush_all (); exit 1 |