X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibraryClean.ml;h=a544991e85b109e3df0f74f68b27efaf04c612e5;hb=9897efac755aac85095075b7e0a967fe340092c1;hp=04333fc9a66724230fea843153a4d36d22d42e3b;hpb=d4c6f8464dc183326b7f7b4dc6171e69b482a26b;p=helm.git diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml index 04333fc9a..a544991e8 100644 --- a/components/library/libraryClean.ml +++ b/components/library/libraryClean.ml @@ -212,15 +212,20 @@ let clean_baseuris ?(verbose=true) buris = 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 ->