]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/libraryClean.ml
tests are now handled with a standard Makefile that does not use do_tests.sh
[helm.git] / helm / software / components / library / libraryClean.ml
index 04333fc9a66724230fea843153a4d36d22d42e3b..2ac65c5c8b9d2f3435a17fdf10a99a82415d6353 100644 (file)
@@ -213,11 +213,14 @@ let clean_baseuris ?(verbose=true) buris =
    (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)));