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/Frontend.mli | |
parent | c1f7436d3e5e65c956fb7e5976e308a83f4d68bb (diff) | |
download | compcert-a48f857450950b2d1370249bca673ad2c15559d1.tar.gz compcert-a48f857450950b2d1370249bca673ad2c15559d1.zip |
Also exit on errors. Bug 19872
Diffstat (limited to 'driver/Frontend.mli')
0 files changed, 0 insertions, 0 deletions