aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driveraux.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2022-05-06 12:54:34 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-05-18 14:22:32 +0200
commit413bd7681ed70155b7bbc9ab2255801ed41904ea (patch)
treef68f78cbdb3c6c81510973f50e7e9a8ac173c0b7 /driver/Driveraux.mli
parent713b45c5d9e497756a414c049fc255aacc3650c2 (diff)
downloadcompcert-413bd7681ed70155b7bbc9ab2255801ed41904ea.tar.gz
compcert-413bd7681ed70155b7bbc9ab2255801ed41904ea.zip
Simplify handling of file suffixes.
Since we are sure that all files passed have a valid extension we can use the OCaml function Filename.remove_extension and don't need to pass the suffixes. Bug 33218
Diffstat (limited to 'driver/Driveraux.mli')
-rw-r--r--driver/Driveraux.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli
index 6f0eaddb..47f923f0 100644
--- a/driver/Driveraux.mli
+++ b/driver/Driveraux.mli
@@ -27,7 +27,7 @@ val tmp_file: string -> string
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
+val output_filename: ?final:bool -> string -> suffix: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).
Otherwise, we generate a file in the current directory. *)