diff options
| author | Emilio Jesus Gallego Arias | 2020-05-18 22:12:29 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-19 19:46:56 +0200 |
| commit | fb0caf14daff2e433dfc33ca564d49b26f7e8fb4 (patch) | |
| tree | f521c06d90108790ae58594cb928c5d5efec7299 /vernac | |
| parent | ed0f2f08e31ee4e645aa6e52970ddefc60f1f4f9 (diff) | |
[topfmt] Set formatter + flush fix
Closes #12351.
We set the parameters of the redirect formatter to be same than the
ones in stdout.
I guess the original semantics was to ignore the parameters, so I'm
unsure we want to do this.
While we are a it, we include a fix on the formatter, which _must_ be
flushed before closing its associated channel.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/topfmt.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 2d8734ff7f..a28d8f605b 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -404,6 +404,7 @@ let with_output_to_file fname func input = let channel = open_out (String.concat "." [fname; "out"]) in let old_fmt = !std_ft, !err_ft, !deep_ft in let new_ft = Format.formatter_of_out_channel channel in + set_gp new_ft (get_gp !std_ft); std_ft := new_ft; err_ft := new_ft; deep_ft := new_ft; @@ -412,6 +413,7 @@ let with_output_to_file fname func input = std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; + Format.pp_print_flush new_ft (); close_out channel; output with reraise -> @@ -419,6 +421,7 @@ let with_output_to_file fname func input = std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; + Format.pp_print_flush new_ft (); close_out channel; Exninfo.iraise reraise |