src/Tools/jEdit/src/pretty_text_area.scala
changeset 58835 462ec23aa92f
parent 58766 5bab56d3dcd4
child 59076 65babcd8b0e6
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Oct 30 11:24:53 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Oct 30 15:57:13 2014 +0100
@@ -230,7 +230,7 @@
     key_pressed = (evt: KeyEvent) =>
       {
         evt.getKeyCode match {
-          case KeyEvent.VK_C
+          case KeyEvent.VK_C | KeyEvent.VK_INSERT
           if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
               text_area.getSelectionCount != 0 =>
             Registers.copy(text_area, '$')