author | wenzelm |
Mon, 17 Mar 2014 11:33:09 +0100 | |
changeset 56171 | 15351577da10 |
parent 56170 | 638b29331549 |
child 56172 | 31289387fdf8 |
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Mar 17 10:45:29 2014 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Mon Mar 17 11:33:09 2014 +0100 @@ -246,7 +246,7 @@ } override def propagate(evt: KeyEvent) { JEdit_Lib.propagate_key(view, evt) - input(evt) + if (evt.getID == KeyEvent.KEY_TYPED) input(evt) } override def refocus() { text_area.requestFocus } }