Merge PR coq#18957: Properly flush -time-file at exit

Reviewed-by: ejgallego Co-authored-by: ejgallego <ejgallego@users.noreply.github.com>
ejgallego · Apr 25, 2024 · c5614d0 · c5614d0
2 parents 03d371d + 7530368
commit c5614d0
Showing 1 changed file with 9 additions and 1 deletion.
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
@@ -40,7 +40,15 @@ type time_output =
 
 let make_time_output = function
   | Coqargs.ToFeedback -> ToFeedback
-  | ToFile f -> ToChannel (Format.formatter_of_out_channel (open_out f))
+  | ToFile f ->
+    let ch = open_out f in
+    let fch = Format.formatter_of_out_channel ch in
+    let close () =
+      Format.pp_print_flush fch ();
+      close_out ch
+    in
+    at_exit close;
+    ToChannel fch
 
 module State = struct