]> matita.cs.unibo.it Git - helm.git/commitdiff
use matita.verbosity instead of matita.quiet
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 6 Feb 2006 17:19:52 +0000 (17:19 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 6 Feb 2006 17:19:52 +0000 (17:19 +0000)
matita/matitacLib.ml

index ee09258e07bad2f80fd62af05a1a1810c5e26267..1297a47473839a8e4da1573374000538f5eef994 100644 (file)
@@ -48,7 +48,7 @@ let run_script is eval_function  =
   in
   let slash_n_RE = Pcre.regexp "\\n" in
   let cb = 
-    if Helm_registry.get_bool "matita.quiet" then 
+    if Helm_registry.get_int "matita.verbosity" < 1 then 
       (fun _ _ -> ())
     else 
       (fun grafite_status stm ->
@@ -171,12 +171,12 @@ let main ~mode =
     | `Debug | `Message -> ()
     | `Warning | `Error -> origcb tag s
   in
-  if Helm_registry.get_bool "matita.quiet" then
+  if Helm_registry.get_int "matita.verbosity" < 1 then
     HLog.set_log_callback newcb;
   let matita_debug = Helm_registry.get_bool "matita.debug" in
   try
     let time = Unix.time () in
-    if Helm_registry.get_bool "matita.quiet" then
+    if Helm_registry.get_int "matita.verbosity" < 1 then
       origcb `Message ("compiling " ^ Filename.basename fname ^ "...")
     else
       HLog.message (sprintf "execution of %s started:" fname);