author | wenzelm |
Thu, 30 Oct 2014 15:57:13 +0100 | |
changeset 58835 | 462ec23aa92f |
parent 58832 | ec9550bd5fd7 |
child 58836 | 4037bb00d08e |
--- 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, '$')