From cb06122ec0250d63b18629e4a85f0515831114ce Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 20 Jul 2007 09:32:39 +0000 Subject: [PATCH] Initialization of matita.map_unicode_to_tex moved from matitaGui to matitaInit (so that ocamlc now works again). --- helm/software/matita/matitaGui.ml | 2 -- helm/software/matita/matitaInit.ml | 15 ++++++++------- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 95d0a7631..e9302d5ac 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -1030,8 +1030,6 @@ class gui () = MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem ~callback:(fun enabled -> Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled); - if not (Helm_registry.has "matita.paste_unicode_as_tex") then - Helm_registry.set_bool "matita.paste_unicode_as_tex" false; main#unicodeAsTexMenuItem#set_active (Helm_registry.get_bool "matita.paste_unicode_as_tex"); (* log *) diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 72c8600bb..7ffb67d9f 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/matita/matitaInit.ml @@ -45,13 +45,14 @@ let already_configured s l = let conffile = ref BuildTimeConf.matita_conf let registry_defaults = [ - "matita.debug", "false"; - "matita.external_editor", "gvim -f -c 'go %p' %f"; - "matita.preserve", "false"; - "matita.profile", "true"; - "matita.system", "false"; - "matita.verbosity", "1"; - "matita.bench", "false"; + "matita.debug", "false"; + "matita.external_editor", "gvim -f -c 'go %p' %f"; + "matita.preserve", "false"; + "matita.profile", "true"; + "matita.system", "false"; + "matita.verbosity", "1"; + "matita.bench", "false"; + "matita.paste_unicode_as_tex", "false" (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is * intuitively verbose *) ] -- 2.39.2