diff options
| -rw-r--r-- | driver/Driver.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 145de6c5..998c67ff 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -537,5 +537,6 @@ let _ = if (not nolink) && linker_args <> [] then begin linker (output_filename_default "a.out") linker_args end; + Cerrors.check_errors () with Sys_error msg -> eprintf "I/O error: %s.\n" msg; exit 2 |