diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 18:18:00 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 18:18:00 +0200 |
| commit | 5f3954b8d919a8fd89ce2332261698f41bc33550 (patch) | |
| tree | d4c7ada4f9e813bddaa3bb1d1e46658e345a774f /toplevel | |
| parent | cb41d7b40c401c15e9cb66f508f89dbd1bdcdbff (diff) | |
| parent | b89c8f3846e8254651dbcba262f83d3d1fe3adb6 (diff) | |
Merge PR#758: [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 d4146ace1..92730c14d 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 |