aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r--tools/coqdep_common.ml1
1 files changed, 0 insertions, 1 deletions
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