From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Jul 2006 11:31:34 +0000 (+0000)
Subject: libraryclean fixed to eradicate files generated from .ma files that do not
X-Git-Tag: 0.4.95@7852~1198
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d3f5ece275f78000b9fb4623ee33715e6e9442d1;p=helm.git

libraryclean fixed to eradicate files generated from .ma files that do not
declare any object (e.g. legacy/coq.ma)
---

diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml
index 2ac65c5c8..a544991e8 100644
--- a/components/library/libraryClean.ml
+++ b/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 ->