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 | |
| parent | b49feed2f88c0a6ae9cc2ca4b2982096f18a2112 (diff) | |
| download | compcert-39bca2093650f3dbe18e60ad19818b939a96b971.tar.gz compcert-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.
| -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 |