X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibraryClean.ml;h=2ac65c5c8b9d2f3435a17fdf10a99a82415d6353;hb=cfea6dbbb5f488f85e4cd7069d5c9179a2ed0b2d;hp=8b32e97c4fa28cc1467298cb41247225ca05002c;hpb=ee3f8d6fa92b051394a2ff7c71c03ac33a05182b;p=helm.git

diff --git a/helm/software/components/library/libraryClean.ml b/helm/software/components/library/libraryClean.ml
index 8b32e97c4..2ac65c5c8 100644
--- a/helm/software/components/library/libraryClean.ml
+++ b/helm/software/components/library/libraryClean.ml
@@ -213,11 +213,14 @@ let clean_baseuris ?(verbose=true) buris =
    (fun baseuri ->
      try 
        HExtlib.safe_remove 
-         (LibraryMisc.obj_file_of_baseuri ~writable:true ~baseuri);
+         (LibraryMisc.obj_file_of_baseuri 
+           ~must_exist:false ~writable:true ~baseuri);
        HExtlib.safe_remove 
-         (LibraryMisc.metadata_file_of_baseuri ~writable:true ~baseuri);
+         (LibraryMisc.metadata_file_of_baseuri 
+           ~must_exist:false ~writable:true ~baseuri);
        HExtlib.safe_remove 
-         (LibraryMisc.lexicon_file_of_baseuri ~writable:true ~baseuri)
+         (LibraryMisc.lexicon_file_of_baseuri 
+           ~must_exist:false ~writable:true ~baseuri)
      with Http_getter_types.Key_not_found _ -> ())
    (HExtlib.list_uniq (List.fast_sort Pervasives.compare
      (List.map (UriManager.buri_of_uri) l)));
@@ -227,7 +230,10 @@ let clean_baseuris ?(verbose=true) buris =
      let buri = UriManager.buri_of_uri uri in
      if buri <> !last_baseuri then
       begin
-       HLog.message ("Removing: " ^ buri ^ "/*");
+        if Helm_registry.get_bool "matita.bench" then
+            (print_endline ("matitaclean " ^ buri ^ "/");flush stdout)
+          else 
+            HLog.message ("Removing: " ^ buri ^ "/*");
        last_baseuri := buri
       end;
      LibrarySync.remove_obj uri