From cb37784d2ad3f641af6d3555c0f62050f6543d0d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 4 May 2018 13:59:59 +0200
Subject: 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.
---
 tools/coqdep_common.ml | 12 +++++++++++-
 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)
-- 
cgit v1.2.3