aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
diff options
context:
space:
mode:
Diffstat (limited to 'exportclight')
-rw-r--r--exportclight/Clightgen.ml2
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