src/Tools/jEdit/src/completion_popup.scala
changeset 53237 6bfe54791591
parent 53236 837a6ef61fe9
child 53242 142f4fff4e40
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:20:11 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:23:40 2013 +0200
     1.3 @@ -186,7 +186,6 @@
     1.4  
     1.5    private val key_listener =
     1.6      JEdit_Lib.key_listener(
     1.7 -      workaround = false,
     1.8        key_pressed = (e: KeyEvent) =>
     1.9          {
    1.10            if (!e.isConsumed) {