- probe: recursive removal of empty directories

[helm.git] / matita / components / binaries / probe / matitaRemove.ml

diff --git a/matita/components/binaries/probe/matitaRemove.ml b/matita/components/binaries/probe/matitaRemove.ml
index 1ef87a5ca16efd829c127ca20c104b3760cf64fc..0ad0cd1d4b3fcc67fda75c2d1f101b138dad5394 100644 (file)
--- a/matita/components/binaries/probe/matitaRemove.ml
+++ b/matita/components/binaries/probe/matitaRemove.ml
@@ -17,10 +17,14 @@ module U = Unix
 module O = Options
 
 let remove_dir dir =
+   let map name = Y.remove (F.concat dir name) in
+   let rec rmdir dir =
+      U.rmdir dir; (* Sys.remove does not seem to remove empty directories *)
+      rmdir (F.dirname dir)
+   in
    if Y.file_exists dir then begin
-      let map name = Y.remove (F.concat dir name) in
       A.iter map (Y.readdir dir);
-      U.rmdir dir (* Sys.remove does not seem to remove empty directories *)
+      try rmdir dir with U.Unix_error _ -> ()
    end
 
 let objects () =