more work for the release

[helm.git] / helm / software / components / library / libraryClean.ml

diff --git a/helm/software/components/library/libraryClean.ml b/helm/software/components/library/libraryClean.ml
index 8b32e97c4fa28cc1467298cb41247225ca05002c..04333fc9a66724230fea843153a4d36d22d42e3b 100644 (file)
--- a/helm/software/components/library/libraryClean.ml
+++ b/helm/software/components/library/libraryClean.ml
@@ -227,7 +227,10 @@ let clean_baseuris ?(verbose=true) buris =
      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