diff options
Diffstat (limited to 'driver/Driveraux.ml')
| -rw-r--r-- | driver/Driveraux.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 5b2d792e..4b9809a6 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -89,12 +89,12 @@ let command_error n exc = and if this is the final destination file (not a dump file). Otherwise, we generate a file in the current directory. *) -let output_filename ?(final = false) source_file source_suffix output_suffix = +let output_filename ?(final = false) source_file ~suffix = match !option_o with | Some file when final -> file | _ -> - Filename.basename (Filename.chop_suffix source_file source_suffix) - ^ output_suffix + Filename.basename (Filename.remove_extension source_file) + ^ suffix (* A variant of [output_filename] where the default output name is fixed *) |