From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Jul 2006 11:39:18 +0000 (+0000)
Subject: rmdir_descend now works also on non existent dirs
X-Git-Tag: make_still_working~7056
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=4b18357deddbebc2fef6187b8810e7a343b9813b;p=helm.git

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 b36a4d89d..32f33bd2b 100644
--- 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 _ -> ()