MatitacleanLib.remove_baseuris will remove empty directories.

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

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 3383ee312e0df59e3fd0f9195eb0f1591184eaf2..f2c9d6e336858c9d236524a5752c81ce1f00ce09 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -306,7 +306,9 @@ let remove ?(verbose=false) uri =
             MatitaLog.debug ("Removing: " ^ baseuri ^ "/*");
             last_baseuri := baseuri
            end;
-        MatitaMisc.safe_remove (Http_getter.resolve' uri)
+           let file = Http_getter.resolve' uri in
+           MatitaMisc.safe_remove file;
+           MatitaMisc.rmdir_descend (Filename.dirname file)
       with Http_getter_types.Key_not_found _ -> ());
       remove_coercion uri; 
       ignore (MatitaDb.remove_uri uri);