Join GitHub today
GitHub is home to over 36 million developers working together to host and review code, manage projects, and build software together.Sign up
Format only flushes std_formatter by at_exit. #7235
Original bug ID: 7235
I have just noticed that the following code of stdlib/format.ml:
(* Output everything left in the pretty printer queue at end of execution. *)
This code only flushes Format.std_formatter. I am not sure it is easily possible to flush all the formatters associated with out_channels alive when at_exit is called but at least we can flush Format.err_formatter here too.
Comment author: @pierreweis
Thank for the report.
Indeed, we should also flush err_formatter at end of program.
Extending this benavior to all formatters created by the library is more problematic since it could lead to excessive memory consumption (keeping track of all allocated formatters in a list or adding a closure for each new formatter to the list of thunks to execute at exit).