# HG changeset patch
# User wenzelm
# Date 1460629064 -7200
# Node ID f17602cbf76a12b53afad49bed941ec67f2467e6
# Parent  744266e32612b383106e2a423d30a6dc904c8908
tuned;

diff -r 744266e32612 -r f17602cbf76a src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Apr 14 12:08:38 2016 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Apr 14 12:17:44 2016 +0200
@@ -78,7 +78,7 @@
 
     val entries =
       new Logic_Entry("", "default (" + session_name() + ")") ::
-        JEdit_Sessions.session_list().map(name => new Logic_Entry(name, name))
+        session_list().map(name => new Logic_Entry(name, name))
 
     val component = new ComboBox(entries) with Option_Component {
       name = option_name