src/Tools/jEdit/src/completion_popup.scala
changeset 53987 16a0cd5293d9
parent 53851 86c8f15afd88
child 54376 3eb84b6b0353
--- a/src/Tools/jEdit/src/completion_popup.scala	Sun Sep 29 16:01:22 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Sep 29 18:51:01 2013 +0200
@@ -259,6 +259,7 @@
               content.substring(0, caret - len) +
               item.replacement +
               content.substring(caret))
+            text_field.getCaret.setDot(caret - len + item.replacement.length)
           case _ =>
         }
       }