aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Diagnostics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'cparser/Diagnostics.ml')
-rw-r--r--cparser/Diagnostics.ml4
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