diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-04 13:28:08 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 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 25e4d79c4..f15021c65 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 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 diff --git a/lib/system.mli b/lib/system.mli index 4dbb3695d..214369095 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 cc63c13d7..0064aebda 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 |