diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-12-15 14:42:30 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-12-15 14:42:30 +0100 |
| commit | a48f857450950b2d1370249bca673ad2c15559d1 (patch) | |
| tree | d454bdda420db55957f346baf1626a66ac1964c1 /driver | |
| parent | c1f7436d3e5e65c956fb7e5976e308a83f4d68bb (diff) | |
| download | compcert-a48f857450950b2d1370249bca673ad2c15559d1.tar.gz compcert-a48f857450950b2d1370249bca673ad2c15559d1.zip | |
Also exit on errors. Bug 19872
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 998c67ff..353a7176 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -537,6 +537,6 @@ let _ = if (not nolink) && linker_args <> [] then begin linker (output_filename_default "a.out") linker_args end; - Cerrors.check_errors () + if Cerrors.check_errors () then exit 2 with Sys_error msg -> eprintf "I/O error: %s.\n" msg; exit 2 |