diff options
| author | Gaëtan Gilbert | 2018-05-04 13:59:59 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-04 14:01:13 +0200 |
| commit | cb37784d2ad3f641af6d3555c0f62050f6543d0d (patch) | |
| tree | 003dbd5db0cac85c0c5e7db10a1e2cab001b1519 /dev/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 'dev/tools')
0 files changed, 0 insertions, 0 deletions