src/Tools/jEdit/src/completion_popup.scala
changeset 56171 15351577da10
parent 56170 638b29331549
child 56173 62f10624339a
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 10:45:29 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 11:33:09 2014 +0100
     1.3 @@ -246,7 +246,7 @@
     1.4                }
     1.5                override def propagate(evt: KeyEvent) {
     1.6                  JEdit_Lib.propagate_key(view, evt)
     1.7 -                input(evt)
     1.8 +                if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
     1.9                }
    1.10                override def refocus() { text_area.requestFocus }
    1.11              }