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 /tools | |
| 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 'tools')
| -rw-r--r-- | tools/coqdep_common.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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 |