diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/aux_file.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 0f0f09aa23..c6c7b42429 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -17,10 +17,6 @@ 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" |