diff options
| author | Maxime Dénès | 2016-11-04 13:28:08 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-04 13:34:14 +0100 |
| commit | 1d637f15de540c82289d6b3a16181a625a0d9cdf (patch) | |
| tree | cbf76bb5af22b0f353d7402ea51f90e297d5d35b | |
| parent | dd1f54e9123646964a842ff2401563a549822783 (diff) | |
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).
| -rw-r--r-- | lib/minisys.ml | 8 | ||||
| -rw-r--r-- | lib/system.ml | 1 | ||||
| -rw-r--r-- | lib/system.mli | 5 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 1 |
4 files changed, 0 insertions, 15 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 *) 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 |