#6 Possible NullPointerException in jEdit plugin

[Trevor Harmon]

There is a possible bug in the jEdit plugin that could occur when the option pane settings have never been saved to disk. This could cause a NullPointerException because the option variables would not be initialized.