From 3e8f729a0e48566f9d1941cad2feec099880665f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 19 Jul 2005 17:24:48 +0000 Subject: [PATCH] Unuseful code removed. --- helm/matita/matitaGui.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 38f8cb784..65a18df55 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -228,7 +228,6 @@ class gui () = if mark_iter#offset < locked_iter_offset then begin source_view#buffer#move_mark `INSERT ~where:mark_iter; - source_view#buffer#move_mark `SEL_BOUND ~where:mark_iter; (MatitaScript.instance ())#goto `Cursor (); end; (* phase 4: we perform again the undo. This time we are sure that -- 2.39.2