diff -r 837a6ef61fe9 -r 6bfe54791591 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Tue Aug 27 22:20:11 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Tue Aug 27 22:23:40 2013 +0200 @@ -186,7 +186,6 @@ private val key_listener = JEdit_Lib.key_listener( - workaround = false, key_pressed = (e: KeyEvent) => { if (!e.isConsumed) {