diff options
Diffstat (limited to 'driver/Driver.ml')
-rwxr-xr-x | driver/Driver.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index e3b9ec52..8fc52e0c 100755 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -552,3 +552,5 @@ let _ = if Cerrors.check_errors () then exit 2 with Sys_error msg -> eprintf "I/O error: %s.\n" msg; exit 2 + | e -> + Cerrors.crash e |