# HG changeset patch
# User wenzelm
# Date 1668022252 -3600
# Node ID 2dfc8885c0ee21cb5ce42f5839febb942dd3aac3
# Parent  e228be7cd3751c4b1d8445b0b26854861a20fa38
tuned GUI;

diff -r e228be7cd375 -r 2dfc8885c0ee src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 09 19:42:21 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 09 20:30:52 2022 +0100
@@ -81,7 +81,7 @@
       val main_sessions = all_sessions.filter(name => sessions(name).main_group)
 
       main_sessions.map(GUI.Selector.item) ::: List(GUI.Selector.separator) :::
-      all_sessions.map(GUI.Selector.item)
+      all_sessions.sorted.map(GUI.Selector.item)
     }
 
     new GUI.Selector(default_entry :: session_entries) with JEdit_Options.Entry {