if system_mode then HLog.message "Compiling in system space";
(* here we go *)
if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
if system_mode then HLog.message "Compiling in system space";
(* here we go *)
if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();