From 622a76e7473084ea2dafb34cbc52fb7756b809b2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 18 Jul 2006 11:31:34 +0000 Subject: [PATCH] libraryclean fixed to eradicate files generated from .ma files that do not declare any object (e.g. legacy/coq.ma) --- helm/software/components/library/libraryClean.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/helm/software/components/library/libraryClean.ml b/helm/software/components/library/libraryClean.ml index 2ac65c5c8..a544991e8 100644 --- a/helm/software/components/library/libraryClean.ml +++ b/helm/software/components/library/libraryClean.ml @@ -212,18 +212,20 @@ let clean_baseuris ?(verbose=true) buris = List.iter (fun baseuri -> try - HExtlib.safe_remove - (LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~writable:true ~baseuri); + let obj_file = + LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri + in + HExtlib.safe_remove obj_file ; HExtlib.safe_remove (LibraryMisc.metadata_file_of_baseuri - ~must_exist:false ~writable:true ~baseuri); + ~must_exist:false ~writable:true ~baseuri) ; HExtlib.safe_remove (LibraryMisc.lexicon_file_of_baseuri - ~must_exist:false ~writable:true ~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 -> -- 2.39.2