changeset 73340 | 0ffcad1f6130 |
parent 73337 | 0af9e7e4476f |
child 75393 | 87ebf5a50283 |
--- a/src/Tools/jEdit/src/jedit_options.scala Mon Mar 01 20:12:09 2021 +0100 +++ b/src/Tools/jEdit/src/jedit_options.scala Mon Mar 01 22:22:12 2021 +0100 @@ -44,7 +44,7 @@ PIDE.session.update_options(PIDE.options.value) } } - def load() { selected = stored } + def load(): Unit = { selected = stored } load() } }