diff options
Diffstat (limited to 'tools/coqdep_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 70c983175..db69a3b79 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -102,8 +102,18 @@ let safe_hash_add cmp clq q (k, (v, b)) = For the ML files, the string is the basename without extension. *) +let same_path_opt s s' = + let nf s = (* ./foo/a.ml and foo/a.ml are the same file *) + if Filename.is_implicit s + then "." // s + else s + in + let s = match s with None -> "." | Some s -> nf s in + let s' = match s' with None -> "." | Some s' -> nf s' in + s = s' + let warning_ml_clash x s suff s' suff' = - if suff = suff' then + if suff = suff' && not (same_path_opt s s') then eprintf "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff (match s with None -> "." | Some d -> d) |