diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-02-15 08:50:18 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-02-15 08:50:18 +0100 |
| commit | 773058e7e21fa76097000bec6f1b9ff7e51d3b84 (patch) | |
| tree | 11e25e755d0a0d63be99883068b573ce41a14370 /driver | |
| parent | f65abd772e574adf0493336a32fb4ea1fe230a8d (diff) | |
| download | compcert-773058e7e21fa76097000bec6f1b9ff7e51d3b84.tar.gz compcert-773058e7e21fa76097000bec6f1b9ff7e51d3b84.zip | |
Fixed regression introduced by refactoring of Driver.ml.
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 83078256..cc0d018e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -293,11 +293,15 @@ let process_c_file sourcename = if !option_interp then begin Machine.config := Machine.compcert_interpreter !Machine.config; let csyntax,_ = parse_c_file sourcename preproname in - Interp.execute csyntax; + if not !option_dprepro then + safe_remove preproname; + Interp.execute csyntax; "" end else if !option_S then begin compile_c_file sourcename preproname (output_filename ~final:true sourcename ".c" ".s"); + if not !option_dprepro then + safe_remove preproname; "" end else begin let asmname = @@ -305,13 +309,13 @@ let process_c_file sourcename = then output_filename sourcename ".c" ".s" else Filename.temp_file "compcert" ".s" in compile_c_file sourcename preproname asmname; + if not !option_dprepro then + safe_remove preproname; let objname = output_filename ~final: !option_c sourcename ".c" ".o" in assemble asmname objname; if not !option_dasm then safe_remove asmname; objname end in - if not !option_dprepro then - safe_remove preproname; if !dump_options then Optionsprinter.print (output_filename sourcename ".c" ".opt.json") !stdlib_path; name |