--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Feb 03 16:24:46 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Feb 03 16:50:14 2023 +0100
@@ -98,7 +98,9 @@
options.value.check_name(option_name).title_jedit
override def load(): Unit = {
val value = options.string(option_name)
- for (entry <- find_value(_ == value)) selection.item = entry
+ for (entry <- find_value(_ == value) if selection.item != entry) {
+ selection.item = entry
+ }
}
override def save(): Unit =
for (value <- selection_value) options.string(option_name) = value