From 1d637f15de540c82289d6b3a16181a625a0d9cdf Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 4 Nov 2016 13:28:08 +0100
Subject: 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).
---
 tools/coqdep_common.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index cc63c13d7b..0064aebdae 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -526,7 +526,6 @@ let rec add_directory recur add_file phys_dir log_dir =
     | FileRegular f ->
         add_file phys_dir log_dir f
   in
-  check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir;
   if exists_dir phys_dir then
     process_directory f phys_dir
   else
-- 
cgit v1.2.3