aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driveraux.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2018-01-03 16:26:14 +0100
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-01-03 16:26:14 +0100
commitca9219d447c37038063f3d297c8f8195bb23e2f1 (patch)
treee67aee7fa6cea3cbfc242818fd2637e072ce2c02 /driver/Driveraux.ml
parent87558f62b29ee94392c3955434aa2680aaaeffa5 (diff)
downloadcompcert-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 'driver/Driveraux.ml')
-rw-r--r--driver/Driveraux.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index 2c478fb1..6d8d0adc 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -18,6 +18,11 @@ open Clflags
let safe_remove file =
try Sys.remove file with Sys_error _ -> ()
+let tmp_file suff =
+ let tmpfile = Filename.temp_file "compcert" suff in
+ at_exit (fun () -> safe_remove tmpfile);
+ tmpfile
+
(* Invocation of external tools *)
let rec waitpid_no_intr pid =