aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
diff options
context:
space:
mode:
authorGuillaume Melquiond2015-12-09 14:56:17 +0100
committerGuillaume Melquiond2015-12-09 14:58:36 +0100
commit9d45d45f3a8718581a001af4576ca87feb741073 (patch)
tree8508ff2281e9e3a985a07a1cad69eca8968de5d4 /lib/system.ml
parentce9e7c2a842d7ec7734b58af64de9283de963e37 (diff)
Remove remaining occurrences of Unix.readdir.
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml30
1 files changed, 10 insertions, 20 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 91b2f5afaf..f860bd2f7e 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -11,12 +11,11 @@
open Pp
open Errors
open Util
-open Unix
(* All subdirectories, recursively *)
let exists_dir dir =
- try let _ = closedir (opendir dir) in true with Unix_error _ -> false
+ try Sys.is_directory dir with Sys_error _ -> false
let skipped_dirnames = ref ["CVS"; "_darcs"]
@@ -31,24 +30,15 @@ let all_subdirs ~unix_path:root =
let l = ref [] in
let add f rel = l := (f, rel) :: !l in
let rec traverse dir rel =
- let dirh = opendir dir in
- try
- while true do
- let f = readdir dirh in
- if ok_dirname f then
- let file = Filename.concat dir f in
- try
- begin match (stat file).st_kind with
- | S_DIR ->
- let newrel = rel @ [f] in
- add file newrel;
- traverse file newrel
- | _ -> ()
- end
- with Unix_error (e,s1,s2) -> ()
- done
- with End_of_file ->
- closedir dirh
+ Array.iter (fun f ->
+ if ok_dirname f then
+ let file = Filename.concat dir f in
+ if Sys.is_directory file then begin
+ let newrel = rel @ [f] in
+ add file newrel;
+ traverse file newrel
+ end)
+ (Sys.readdir dir)
in
if exists_dir root then traverse root [];
List.rev !l