From 857e746959f1eb9d0158073114d5ae0aa1c2fc1f Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 9 Feb 2018 09:53:12 +0100
Subject: Added error summary in case of fatal error.

---
 driver/Driver.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'driver/Driver.ml')

diff --git a/driver/Driver.ml b/driver/Driver.ml
index 9c9f2d79..0ad820ea 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -415,5 +415,5 @@ let _ =
   with
   | Sys_error msg
   | CmdError msg -> error no_loc "%s" msg; exit 2
-  | Abort -> exit 2
+  | Abort -> error_summary (); exit 2
   | e -> crash e
-- 
cgit