author | wenzelm |
Thu, 14 Apr 2016 12:17:44 +0200 | |
changeset 62974 | f17602cbf76a |
parent 62973 | 744266e32612 |
child 62975 | 1d066f6ab25d |
child 62978 | c04eead96cca |
--- 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