| changeset 69854 | cc0b3e177b49 |
| parent 69759 | 092c6a4bcc26 |
| child 70775 | 97d3485028b6 |
--- a/src/Tools/jEdit/src/plugin.scala Fri Mar 01 20:16:26 2019 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Fri Mar 01 21:29:59 2019 +0100 @@ -65,7 +65,8 @@ /* options */ private var _options: JEdit_Options = null - private def init_options(): Unit = _options = new JEdit_Options(Options.init()) + private def init_options(): Unit = + _options = new JEdit_Options(Options.init()) def options: JEdit_Options = _options