author | wenzelm |
Sun, 18 Sep 2011 21:15:31 +0200 | |
changeset 44981 | 2bec3b7514cf |
parent 44980 | ad5883642a83 |
child 44982 | e7ac11643bef |
--- a/src/Tools/jEdit/src/session_dockable.scala Sun Sep 18 20:26:08 2011 +0200 +++ b/src/Tools/jEdit/src/session_dockable.scala Sun Sep 18 21:15:31 2011 +0200 @@ -130,7 +130,7 @@ component.background = list.background component.foreground = list.foreground component.node_name = name - component.text = name.theory + component.text = name.theory + " " } } status.renderer = new Node_Renderer