diff options
| author | Guillaume Melquiond | 2015-12-09 14:56:17 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-12-09 14:58:36 +0100 |
| commit | 9d45d45f3a8718581a001af4576ca87feb741073 (patch) | |
| tree | 8508ff2281e9e3a985a07a1cad69eca8968de5d4 /lib | |
| parent | ce9e7c2a842d7ec7734b58af64de9283de963e37 (diff) | |
Remove remaining occurrences of Unix.readdir.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 30 |
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 |
