# HG changeset patch
# User wenzelm
# Date 1675439414 -3600
# Node ID 45b9bbe6e3750ab8ffc99b3e845da59ad5e3e231
# Parent  25dbf5bec91e22264c3dd80d9512f26ec37e1970
avoid redundant SelectionChanged events;

diff -r 25dbf5bec91e -r 45b9bbe6e375 src/Tools/jEdit/src/jedit_sessions.scala
--- 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