hardwired imitation of copy.shortcut2 default;
authorwenzelm
Thu, 30 Oct 2014 15:57:13 +0100
changeset 58835 462ec23aa92f
parent 58832 ec9550bd5fd7
child 58836 4037bb00d08e
hardwired imitation of copy.shortcut2 default;
src/Tools/jEdit/src/pretty_text_area.scala
--- 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, '$')