From cb06122ec0250d63b18629e4a85f0515831114ce Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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.5