rmdir_descend now works also on non existent dirs

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index b36a4d89db2630f5d0d192454f706d86fa1054d3..32f33bd2be735bbb3d5df18d4d63cc0c62e863e9 100644 (file)
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -314,13 +314,16 @@ let find ?(test = fun _ -> true) path =
 let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
 
 let is_dir_empty d =
- let od = Unix.opendir d in
- let rec aux () =
-  let name = Unix.readdir od in
-  if name <> "." && name <> ".." then false else aux () in
- let res = try aux () with End_of_file -> true in
-  Unix.closedir od;
-  res
+ try
+  let od = Unix.opendir d in
+  let rec aux () =
+   let name = Unix.readdir od in
+   if name <> "." && name <> ".." then false else aux () in
+  let res = try aux () with End_of_file -> true in
+   Unix.closedir od;
+   res
+ with
+  Unix.Unix_error _ -> true (* raised by Unix.opendir, we hope :-) *)
 
 let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> ()