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) {