From 9ffc433e8913660620b1dd4ce4c22db1e42c7562 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 10 Jan 2006 12:12:18 +0000
Subject: [PATCH] Dead code removed.

---
 helm/matita/matitaGui.ml | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 4ca67368f..03e50588f 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -725,12 +725,6 @@ class gui () =
       let top = locker (keep_focus top) in
       let bottom = locker (keep_focus bottom) in
       let jump = locker (keep_focus jump) in
-      let connect_key sym f =
-        connect_key main#mainWinEventBox#event
-          ~modifiers:[`CONTROL] ~stop:true sym f;
-        connect_key self#sourceView#event
-          ~modifiers:[`CONTROL] ~stop:true sym f
-      in
         (* quit *)
       self#setQuitCallback (fun () -> 
         let lexicon_status = (MatitaScript.current ())#lexicon_status in
-- 
2.39.2