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 /lib/system.ml | |
| 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).
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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 |