From 77bcabbc36c54f3146882885c84b940622da9314 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 8 Jan 2019 13:41:11 +0100
Subject: Fix #3934: coqc -time -quick gives unreadable output

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

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 32c6c7d959..bed7b4d42a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2017,7 +2017,7 @@ end = struct (* {{{ *)
       find ~time:false ~batch:false ~fail:false e in
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
     Vernacentries.with_fail st fail (fun () ->
-    (if time then System.with_time ~batch else (fun x -> x)) (fun () ->
+    (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Proof_global.with_current_proof (fun _ p ->
       let Proof.{goals} = Proof.data p in
-- 
cgit v1.2.3