summaryrefslogtreecommitdiff
path: root/checker/checker.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/checker.ml')
-rw-r--r--checker/checker.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index 945abde4..e5e20b1a 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -371,7 +371,8 @@ let run () =
compile_files ();
flush_all()
with e ->
- (Pp.ppnl(explain_exn e);
+ (flush_all();
+ Pp.ppnl(explain_exn e);
flush_all();
exit 1)