From 831f51f3a0a972c741705dcc3244e79fe6c1b634 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 21 Jul 2008 11:47:15 +0000 Subject: [PATCH] add conf key matita.debug_menu --- helm/software/matita/matita.ml | 4 +++- helm/software/matita/matitaInit.ml | 1 + 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index b39eb8531..62e425bf3 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -105,7 +105,9 @@ let _ = (** {{{ Debugging *) let _ = - if BuildTimeConf.debug then begin + if BuildTimeConf.debug || + Helm_registry.get_bool "matita.debug_menu" + then begin gui#main#debugMenu#misc#show (); let addDebugItem ~label callback = let item = diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 705108aa6..d8d498a32 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/matita/matitaInit.ml @@ -44,6 +44,7 @@ let conffile = ref BuildTimeConf.matita_conf let registry_defaults = [ "matita.debug", "false"; + "matita.debug_menu", "false"; "matita.external_editor", "gvim -f -c 'go %p' %f"; "matita.profile", "true"; "matita.system", "false"; -- 2.39.2