diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-02-09 09:53:12 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-02-09 09:53:12 +0100 |
| commit | 857e746959f1eb9d0158073114d5ae0aa1c2fc1f (patch) | |
| tree | 63e38025de7e855da2e3aec1a5220de03313dd1d /driver | |
| parent | d8da506981905752f84165f622fdf0ee26011744 (diff) | |
| download | compcert-857e746959f1eb9d0158073114d5ae0aa1c2fc1f.tar.gz compcert-857e746959f1eb9d0158073114d5ae0aa1c2fc1f.zip | |
Added error summary in case of fatal error.
Diffstat (limited to 'driver')
| -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 |