X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.ml;h=8552cbf8629ba98f72086fd58c11d67512bd9d49;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=a10594ab2a68ebf3f0f909d4140ce2ae165c86c5;hpb=595d77eece3202a799e786ac5996b6b1e25fac6e;p=helm.git diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index a10594ab2..8552cbf86 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -140,6 +140,7 @@ let main ~mode = in if Helm_registry.get_bool "matita.quiet" then MatitaLog.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 @@ -181,7 +182,7 @@ let main ~mode = end else begin - let moo_fname = MatitaMisc.obj_file_of_script fname in + let moo_fname = MatitacleanLib.obj_file_of_script fname in MatitaMoo.save_moo moo_fname moo_content_rev; MatitaLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); @@ -207,7 +208,7 @@ let main ~mode = else pp_ocaml_mode () | exn -> - if Helm_registry.get_bool "matita.debug" then raise exn; + if matita_debug then raise exn; if mode = `COMPILER then clean_exit (Some 3) else