# HG changeset patch
# User wenzelm
# Date 1610149986 -3600
# Node ID 918f6c8b1f150e4de178db6b7e2837098e179936
# Parent  efc58b56a6c78c5b21e9f275bb9182990b8acc49
tuned GUI, notably for scalable FlatLaf;

diff -r efc58b56a6c7 -r 918f6c8b1f15 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sat Jan 09 00:11:52 2021 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Sat Jan 09 00:53:06 2021 +0100
@@ -47,7 +47,7 @@
 
     private val text = new TextArea {
       editable = false
-      columns = 65
+      columns = 60
       rows = 24
     }
     text.font = GUI.copy_font((new Label).font)