changeset 53246 | 8d34caf5bf82 |
parent 53244 | ec6011bf2362 |
child 53272 | 0dfd78ff7696 |
--- a/src/Tools/jEdit/src/plugin.scala Wed Aug 28 10:35:12 2013 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Wed Aug 28 15:14:58 2013 +0200 @@ -57,7 +57,7 @@ def dismissed_popups(view: View): Boolean = { - val b1 = Completion_Popup.dismissed_view(view) + val b1 = Completion_Popup.dismissed(view.getLayeredPane) val b2 = Pretty_Tooltip.dismissed_all() b1 || b2 }