From b89c8f3846e8254651dbcba262f83d3d1fe3adb6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 10 Jun 2017 03:22:24 +0200
Subject: [toplevel] Print error header on fatal batch error.

---
 toplevel/vernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a61ade7849..f0c77875a5 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
 
-- 
cgit v1.2.3