Skip to content

Commit c5614d0

Browse files
Merge PR #18957: Properly flush -time-file at exit
Reviewed-by: ejgallego Co-authored-by: ejgallego <[email protected]>
2 parents 03d371d + 7530368 commit c5614d0

File tree

1 file changed

+9
-1
lines changed

1 file changed

+9
-1
lines changed

toplevel/vernac.ml

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,15 @@ type time_output =
4040

4141
let make_time_output = function
4242
| Coqargs.ToFeedback -> ToFeedback
43-
| ToFile f -> ToChannel (Format.formatter_of_out_channel (open_out f))
43+
| ToFile f ->
44+
let ch = open_out f in
45+
let fch = Format.formatter_of_out_channel ch in
46+
let close () =
47+
Format.pp_print_flush fch ();
48+
close_out ch
49+
in
50+
at_exit close;
51+
ToChannel fch
4452

4553
module State = struct
4654

0 commit comments

Comments
 (0)