diff options
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 48 |
1 files changed, 15 insertions, 33 deletions
diff --git a/lib/system.ml b/lib/system.ml index 73095f9cd6..6c01a270e2 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -12,45 +12,27 @@ open Pp open Errors open Util open Unix +open Systemdirs -(* All subdirectories, recursively *) - -let exists_dir dir = - try let _ = closedir (opendir dir) in true with Unix_error _ -> false - -let skipped_dirnames = ref ["CVS"; "_darcs"] - -let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames - -let ok_dirname f = - not (String.is_empty f) && f.[0] != '.' && - not (String.List.mem f !skipped_dirnames) && - (match Unicode.ident_refutation f with None -> true | _ -> false) +(** Returns the list of all recursive subdirectories of [root] in + depth-first search, with sons ordered as on the file system; + warns if [root] does not exist *) 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 + let rec traverse path rel = + let f = function + | FileDir (path,f) -> + let newrel = rel @ [f] in + add path newrel; + traverse path newrel + | _ -> () + in process_directory f path in - if exists_dir root then traverse root []; + check_unix_dir (fun s -> msg_warning (str s)) root; + if exists_dir root then traverse root [] + else msg_warning (str ("Cannot open " ^ root)); List.rev !l let rec search paths test = |