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).
---
 lib/system.mli | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'lib/system.mli')

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 *)
 
-- 
cgit v1.2.3