From 86e8deed878251e74534393a7b37a1471f7fa079 Mon Sep 17 00:00:00 2001
From: spanjel
Date: Thu, 8 Aug 2019 02:12:31 -0700
Subject: map directory read error to empty directory

---
 lib/system.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/system.ml b/lib/system.ml
index 46b358f825..b1a9efccfc 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -53,8 +53,14 @@ module StrSet = Set.Make(StrMod)
 let dirmap = ref StrMap.empty
 
 let make_dir_table dir =
+  let entries =
+    try
+      Sys.readdir dir
+    with Sys_error _ ->
+      warn_cannot_open_dir dir;
+      [||] in
   let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
-  Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
+  Array.fold_left filter_dotfiles StrSet.empty entries
 
 (** Don't trust in interactive mode (the default) *)
 let trust_file_cache = ref false
-- 
cgit v1.2.3