additional space for borderless UI;
authorwenzelm
Sun, 18 Sep 2011 21:15:31 +0200
changeset 44981 2bec3b7514cf
parent 44980 ad5883642a83
child 44982 e7ac11643bef
additional space for borderless UI;
src/Tools/jEdit/src/session_dockable.scala
--- 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