# HG changeset patch
# User wenzelm
# Date 1316373331 -7200
# Node ID 2bec3b7514cf6961319fdd44b6d8a6b850dfb89b
# Parent  ad5883642a8374be63d78f0f2d74aa18ec28fd32
additional space for borderless UI;

diff -r ad5883642a83 -r 2bec3b7514cf 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