diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-06 04:52:43 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:51:49 +0100 |
| commit | 00b1ceb18db39334a357784a114e45a9012cf594 (patch) | |
| tree | 2866da73af351ee2b41a59028e34b31a10094987 /plugins/extraction/extract_env.ml | |
| parent | 829a8feb3d02da057d39b5029b422e8a45dd1608 (diff) | |
[extraction] Flush formatters at end of output.
Previous implementations of `Pp` flushed on newline, however,
depending on the formatter this may not be always the case.
We now alwayas flush the formatters before closing the file as this is
the intended behavior.
Diffstat (limited to 'plugins/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index ee623c5ca..2b12462ad 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -519,8 +519,10 @@ let print_structure_to_file (fn,si,mo) dry struc = set_phase Impl; pp_with ft (d.preamble mo comment opened unsafe_needs); pp_with ft (d.pp_struct struc); + Format.pp_print_flush ft (); Option.iter close_out cout; with reraise -> + Format.pp_print_flush ft (); Option.iter close_out cout; raise reraise end; if not dry then Option.iter info_file fn; @@ -533,8 +535,10 @@ let print_structure_to_file (fn,si,mo) dry struc = set_phase Intf; pp_with ft (d.sig_preamble mo comment opened unsafe_needs); pp_with ft (d.pp_sig (signature_of_structure struc)); + Format.pp_print_flush ft (); close_out cout; with reraise -> + Format.pp_print_flush ft (); close_out cout; raise reraise end; info_file si) |