diff options
| author | Gaëtan Gilbert | 2020-05-21 14:47:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-21 14:47:45 +0200 |
| commit | 0aedb0c8464d7f84a6fda9ed24290a8341fe8322 (patch) | |
| tree | 21f2c1d6d2d56243b10297cc26ca8e6648060eca /vernac | |
| parent | 7c17979b38bebbc6730cb1b3edf5fa1329f2f001 (diff) | |
| parent | fb0caf14daff2e433dfc33ca564d49b26f7e8fb4 (diff) | |
Merge PR #12358: [topfmt] Set formatter + flush fix
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
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 |