]> matita.cs.unibo.it Git - helm.git/commitdiff
Unuseful code removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 19 Jul 2005 17:24:48 +0000 (17:24 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 19 Jul 2005 17:24:48 +0000 (17:24 +0000)
helm/matita/matitaGui.ml

index 38f8cb7849da4d1af0d5cbf2c5328454c6e8f4da..65a18df55c8e8977516e13498bf5c528b217d994 100644 (file)
@@ -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