diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-01-04 18:35:40 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-01-04 18:35:40 +0100 |
| commit | 8219490aae44fa79932d913cc69941d6b22a70a3 (patch) | |
| tree | b60527a283191e2293a4af3497e48303402ee626 /driver/Driver.ml | |
| parent | b1455cc40ebf6bb00722ff128e702f83c9b4dca8 (diff) | |
| download | compcert-8219490aae44fa79932d913cc69941d6b22a70a3.tar.gz compcert-8219490aae44fa79932d913cc69941d6b22a70a3.zip | |
Handle dcompcertc and dparsedc like all dump opts.
This time with the correct place for setting the destination files.
Bug 20521
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 5afa0a76..b23a4e4f 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -76,7 +76,9 @@ let compile_c_file sourcename ifile ofile = (* Prepare to dump Clight, RTL, etc, if requested *) let set_dest dst opt ext = dst := if !opt then Some (output_filename sourcename ".c" ext) - else None in + else None in + set_dest Cprint.destination option_dparse ".parsed.c"; + set_dest PrintCsyntax.destination option_dcmedium ".compcert.c"; set_dest PrintClight.destination option_dclight ".light.c"; set_dest PrintCminor.destination option_dcminor ".cm"; set_dest PrintRTL.destination option_drtl ".rtl"; |