- hmysql removed (RIP)

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

diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml
index d9ce848d512d3115f901a03c8e5fe6e79b2f4b47..706981937df97aace3cbf6369ff1321912962ad6 100644 (file)
--- a/matita/matita/matitacLib.ml
+++ b/matita/matita/matitacLib.ml
@@ -185,8 +185,7 @@ let compile atstart options fname =
        ~must_exist:false ~baseuri ~writable:true
     in
     (* cleanup of previously compiled objects *)
-    if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
-        LibraryClean.db_uris_of_baseuri baseuri <> []) 
+    if (not (Http_getter_storage.is_empty ~local:true baseuri))
       then begin
       HLog.message ("baseuri " ^ baseuri ^ " is not empty");
       HLog.message ("cleaning baseuri " ^ baseuri);