(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)));
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