src/Tools/jEdit/src/completion_popup.scala
changeset 53293 fd27b8f5a479
parent 53292 f567c1c7b180
child 53296 65c60c782da5
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 21:17:46 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 21:49:46 2013 +0200
     1.3 @@ -155,10 +155,6 @@
     1.4            else input_delay.invoke()
     1.5          }
     1.6        }
     1.7 -      else {
     1.8 -        dismissed()
     1.9 -        input_delay.revoke()
    1.10 -      }
    1.11      }
    1.12  
    1.13      private val input_delay =