diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-05-03 15:41:18 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-05-18 14:22:32 +0200 |
| commit | 713b45c5d9e497756a414c049fc255aacc3650c2 (patch) | |
| tree | 82bc0e33d3b6d7cd6b0f80b1f2d17a8b4cf70955 /driver/Driveraux.ml | |
| parent | 26a9afb1afadfe99d9a799d11569213e5d8db522 (diff) | |
| download | compcert-713b45c5d9e497756a414c049fc255aacc3650c2.tar.gz compcert-713b45c5d9e497756a414c049fc255aacc3650c2.zip | |
Fix computing of output filenames.
At some places the ".c" was hard coded as suffix for computing the
output filenames. This lead to problems if for example `-S`or `-c` is
used with preprocessed files.
Bug 33196
Diffstat (limited to 'driver/Driveraux.ml')
0 files changed, 0 insertions, 0 deletions