diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-01-03 16:26:14 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-01-03 16:26:14 +0100 |
| commit | ca9219d447c37038063f3d297c8f8195bb23e2f1 (patch) | |
| tree | e67aee7fa6cea3cbfc242818fd2637e072ce2c02 /exportclight | |
| parent | 87558f62b29ee94392c3955434aa2680aaaeffa5 (diff) | |
| download | compcert-kvx-ca9219d447c37038063f3d297c8f8195bb23e2f1.tar.gz compcert-kvx-ca9219d447c37038063f3d297c8f8195bb23e2f1.zip | |
Remove all temporary files at program exit (#46)
Replaced calls to Filename.temp_file by own version Driveraux.tmp_file.
The Driveraux.tmp_file function takes care that the temporary files are
removed at exit.
Consequently there is no need to explicitly remove temp files in Driver.
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/Clightgen.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index ae1d09a6..05ece5de 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -69,7 +69,7 @@ let process_c_file sourcename = if !option_E then begin preprocess sourcename "-" end else begin - let preproname = Filename.temp_file "compcert" ".i" in + let preproname = Driveraux.tmp_file ".i" in preprocess sourcename preproname; compile_c_file sourcename preproname (prefixname ^ ".v") end |