diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-05-06 17:00:10 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-05-10 14:32:01 +0200 |
| commit | 39bca2093650f3dbe18e60ad19818b939a96b971 (patch) | |
| tree | 93a876ce57c9d4098dd998b2e53e40d43a48b383 /cparser/Diagnostics.ml | |
| parent | b49feed2f88c0a6ae9cc2ca4b2982096f18a2112 (diff) | |
| download | compcert-kvx-39bca2093650f3dbe18e60ad19818b939a96b971.tar.gz compcert-kvx-39bca2093650f3dbe18e60ad19818b939a96b971.zip | |
Ensure flushing of the error formatter.
Since the error formatter is not automatically flushed at program
exit we need to ensure that it is flushed at exit.
Diffstat (limited to 'cparser/Diagnostics.ml')
| -rw-r--r-- | cparser/Diagnostics.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml index 172affab..2b8a3eb4 100644 --- a/cparser/Diagnostics.ml +++ b/cparser/Diagnostics.ml @@ -18,6 +18,10 @@ open Format open Commandline +(* Ensure that the error formatter is flushed at exit *) +let _ = + at_exit (pp_print_flush err_formatter) + (* Should errors be treated as fatal *) let error_fatal = ref false |