X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitacLib.ml;h=a17845331d84ed0f5bdb5d8252d1aafc68b23545;hb=54e4c7dc896732bafcd907b0380d59efa0a181b7;hp=3c3d421a5f69b8065b0e435aafc53420520d056d;hpb=3c8a3783837bf7773437b12a089b8edf93879b5d;p=helm.git

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 3c3d421a5..a17845331 100644
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -110,7 +110,6 @@ let get_include_paths options =
 let rec compile options fname =
   (* initialization, MOVE OUTSIDE *)
   let matita_debug = Helm_registry.get_bool "matita.debug" in
-  let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in    
   (* sanity checks *)
   let include_paths = get_include_paths options in
   let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in
@@ -125,7 +124,7 @@ let rec compile options fname =
       (Printf.sprintf "uri %s belongs to a read-only repository" baseuri);
   (* cleanup of previously compiled objects *)
   if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
-      LibraryClean.db_uris_of_baseuri baseuri <> []) && clean_baseuri
+      LibraryClean.db_uris_of_baseuri baseuri <> []) 
     then begin
     HLog.message ("baseuri " ^ baseuri ^ " is not empty");
     HLog.message ("cleaning baseuri " ^ baseuri);