diff options
| author | Emilio Jesus Gallego Arias | 2017-02-06 04:52:43 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:51:49 +0100 |
| commit | 00b1ceb18db39334a357784a114e45a9012cf594 (patch) | |
| tree | 2866da73af351ee2b41a59028e34b31a10094987 /kernel/nativecode.mli | |
| 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 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions