From 1d637f15de540c82289d6b3a16181a625a0d9cdf Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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).
---
 lib/system.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'lib/system.ml')

diff --git a/lib/system.ml b/lib/system.ml
index af9aa5c07..4b99de707 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
-- 
cgit v1.2.3