List.iter
(fun baseuri ->
try
+ let obj_file =
+ LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri
+ in
+ HExtlib.safe_remove obj_file ;
HExtlib.safe_remove
- (LibraryMisc.obj_file_of_baseuri ~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) ;
+ HExtlib.rmdir_descend (Filename.chop_extension obj_file)
with Http_getter_types.Key_not_found _ -> ())
(HExtlib.list_uniq (List.fast_sort Pervasives.compare
- (List.map (UriManager.buri_of_uri) l)));
+ (List.map (UriManager.buri_of_uri) l @ buris)));
List.iter
(let last_baseuri = ref "" in
fun uri ->
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