changeset 62974 | f17602cbf76a |
parent 62973 | 744266e32612 |
child 63986 | c7a4b03727ae |
--- 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