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, '$')