diff options
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |