diff options
| -rw-r--r-- | lib/aux_file.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index c6c7b42429..0f0f09aa23 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -17,6 +17,10 @@ let version = 1 let oc = ref None +let chop_extension f = + if check_suffix f ".v" then chop_extension f + else f + let aux_file_name_for vfile = dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux" |