diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-04 13:59:59 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-04 14:01:13 +0200 |
| commit | cb37784d2ad3f641af6d3555c0f62050f6543d0d (patch) | |
| tree | 003dbd5db0cac85c0c5e7db10a1e2cab001b1519 /tools | |
| parent | 90ac335a32afc6bbca5c11b7be7aabc1f7abb89b (diff) | |
Fix #7413: coqdep warning on repeated files
The same warning exists in ocamllibdep so I copied the change there.
Detecting when 2 paths are the same is approximate, eg ././a.ml and
a.ml are considered different. Implementing realpath probably isn't
worth doing for this warning.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep_common.ml | 12 | ||||
| -rw-r--r-- | tools/ocamllibdep.mll | 12 |
2 files changed, 22 insertions, 2 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) diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 125c1452d..382c39d3f 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -116,8 +116,18 @@ let error_cannot_parse s (i,j) = Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j; exit 1 +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) |