tuned GUI, notably for scalable FlatLaf;
authorwenzelm
Sat, 09 Jan 2021 00:53:06 +0100
changeset 73113 918f6c8b1f15
parent 73112 efc58b56a6c7
child 73114 9bf36baa8686
tuned GUI, notably for scalable FlatLaf;
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)