MatitacleanLib.remove_baseuris will remove empty directories.

[helm.git] / helm / matita / matitaMisc.ml

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 9c0c7db33338f6a40e8bc2267d96d43324027c81..e86e4b9a051e33ecfc81ab671b25cc7bd4359c48 100644 (file)
--- 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