From ca9219d447c37038063f3d297c8f8195bb23e2f1 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 3 Jan 2018 16:26:14 +0100 Subject: 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. --- driver/Driveraux.mli | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'driver/Driveraux.mli') diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index 274ecedd..51333b2a 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -22,6 +22,11 @@ val command_error: string -> int -> unit val safe_remove: string -> unit (** Remove the given file if it exists *) +val tmp_file: string -> string + (** Create a temporary file with the given suffix. + The file will be removed when the program exits. + Return the absolute path to the file. *) + val output_filename: ?final:bool -> string -> string -> string -> string (** Determine names for output files. We use -o option if specified and if this is the final destination file (not a dump file). -- cgit