aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/system.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 0f610b8d5..74dd224a0 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