make directory erased, no more -bench since it is the default,

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

diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml
index a1f2a0cfc08fd356437b20a71dd7eea3d5220d48..6998c1cbf1ceee98a6d84e4e43c9307b5a8f98df 100644 (file)
--- a/components/library/libraryClean.ml
+++ b/components/library/libraryClean.ml
@@ -242,7 +242,7 @@ let clean_baseuris ?(verbose=true) buris =
      let buri = UriManager.buri_of_uri uri in
      if buri <> !last_baseuri then
       begin
-        if Helm_registry.get_bool "matita.bench" then
+        if not (Helm_registry.get_bool "matita.verbose") then
             (print_endline ("matitaclean " ^ buri ^ "/");flush stdout)
           else 
             HLog.message ("Removing: " ^ buri ^ "/*");