Fix #4837: ./configure -local makes coqdep issue many warnings

We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).

3 files changed, 0 insertions, 14 deletions

diff --git a/lib/minisys.ml b/lib/minisys.ml
index 25e4d79c4e..f15021c655 100644
--- a/lib/minisys.ml
+++ b/lib/minisys.ml
@@ -46,14 +46,6 @@ let ok_dirname f =
 let exists_dir dir =
   try Sys.is_directory dir with Sys_error _ -> false
 
-let check_unix_dir warn dir =
-  if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
-    (String.length dir > 2 && dir.[1] = ':' ||
-     String.contains dir '\\' ||
-     String.contains dir ';')
-  then warn ("assuming " ^ dir ^
-             " to be a Unix path even if looking like a Win32 path.")
-
 let apply_subdir f path name =
   (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
   (* as well as skipped files like CVS, ... *)
diff --git a/lib/system.ml b/lib/system.ml
index af9aa5c074..4b99de707b 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -33,7 +33,6 @@ let all_subdirs ~unix_path:root =
       | _ -> ()
     in process_directory f path
   in
-  check_unix_dir (fun s -> Feedback.msg_warning (str s)) root;
   if exists_dir root then traverse root []
   else warn_cannot_open_dir root;
   List.rev !l
diff --git a/lib/system.mli b/lib/system.mli
index 4dbb3695d2..214369095c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -20,11 +20,6 @@ val (//) : unix_path -> string -> unix_path
 
 val exists_dir : unix_path -> bool
 
-(** [check_unix_dir warn path] calls [warn] with an appropriate
-     message if [path] looks does not look like a Unix path on Windows *)
-
-val check_unix_dir : (string -> unit) -> unix_path -> unit
-
 (** [exclude_search_in_dirname path] excludes [path] when processing
     directories *)