diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-14 10:44:22 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-14 10:44:22 +0100 |
| commit | d58957f63d36e2da41f6f839a2d94cb0db4c8125 (patch) | |
| tree | 884b79ab00b0b914a4fa2c3335491927eaf86a17 /lib/system.ml | |
| parent | 7ae0748586fe8291f0666cce7bd39d7109471d08 (diff) | |
Remove some occurrences of Unix.opendir.
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/lib/system.ml b/lib/system.ml index b57c02a14..b641aad91 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -64,9 +64,7 @@ let apply_subdir f path name = | _ -> () let process_directory f path = - let dirh = Unix.opendir path in - try while true do apply_subdir f path (Unix.readdir dirh) done - with End_of_file -> Unix.closedir dirh + Array.iter (apply_subdir f path) (Sys.readdir path) let process_subdirectories f path = let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in |