aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2015-12-04 19:25:08 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-12-09 14:58:36 +0100
commitce9e7c2a842d7ec7734b58af64de9283de963e37 (patch)
tree93dcdcbff81fc5f72390e917876a22701fe0b2ee /lib
parent36cbe8fa3bd20469b45b299f66e88e03768a81af (diff)
Replace Unix.readdir by Sys.readdir in dir cache.
This makes the function sightly more portable.
Diffstat (limited to 'lib')
-rw-r--r--lib/system.ml12
1 files changed, 2 insertions, 10 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 2e35a98f7..91b2f5afa 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -67,16 +67,8 @@ module StrSet = Set.Make(StrMod)
let dirmap = ref StrMap.empty
let make_dir_table dir =
- let b = ref StrSet.empty in
- let a = Unix.opendir dir in
- (try
- while true do
- let s = Unix.readdir a in
- if s.[0] != '.' then b := StrSet.add s !b
- done
- with
- | End_of_file -> ());
- Unix.closedir a; !b
+ 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)
let exists_in_dir_respecting_case dir bf =
let contents, cached =