From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 21 Jul 2008 11:47:15 +0000 (+0000)
Subject: add conf key matita.debug_menu
X-Git-Tag: make_still_working~4905
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=831f51f3a0a972c741705dcc3244e79fe6c1b634;p=helm.git

add conf key matita.debug_menu
---

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";