[ jEdit-devel ] Plugin options not appearing

[Slava P. <sl...@je...>]

Hi all,

Some plugins's option panes (PMD, CodeBrowser, TomcatSwitch) fail in pre10 
because I made AbstractOptionPane.init()/save() final. While they should be 
fixed to override _init()/_save() eventually, I will remove the 'final' 
attribute so that things keep working in the next pre-release.
-- 
Slava Pestov