X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=e86e4b9a051e33ecfc81ab671b25cc7bd4359c48;hb=5b17a67ffd16485adf2e66a6241b72e91ed15621;hp=9c0c7db33338f6a40e8bc2267d96d43324027c81;hpb=b2f2e47efe1e01df81cb7659c30eeb76f1f830da;p=helm.git

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 9c0c7db33..e86e4b9a0 100644
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -80,6 +80,28 @@ let is_empty buri =
 
 let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
 
+let is_dir_empty d =
+  try 
+    let od = Unix.opendir d in
+    try 
+      ignore (Unix.readdir od);
+      ignore (Unix.readdir od);
+      ignore (Unix.readdir od);
+      Unix.closedir od;
+      false
+    with End_of_file -> 
+      Unix.closedir od;
+      true
+  with Unix.Unix_error _ -> true
+
+let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> ()
+
+let rec rmdir_descend d = 
+  if is_dir_empty d then
+    begin
+      safe_rmdir d;
+      rmdir_descend (Filename.dirname d)
+    end
 
 let absolute_path file =
   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file