tuned GUI;
authorwenzelm
Wed, 09 Nov 2022 20:30:52 +0100
changeset 76493 2dfc8885c0ee
parent 76492 e228be7cd375
child 76494 9686049ce988
tuned GUI;
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 {