# HG changeset patch
# User wenzelm
# Date 1399412124 -7200
# Node ID 3e8cbb624cc543b5eba69a72c97c60491b881e32
# Parent  1ca814da47aebb4d271d2f18643922204652a37f
tuned GUI for Windows L&F;

diff -r 1ca814da47ae -r 3e8cbb624cc5 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Tue May 06 23:08:18 2014 +0200
+++ b/src/Pure/GUI/gui.scala	Tue May 06 23:35:24 2014 +0200
@@ -140,7 +140,7 @@
 
     makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
     peer.getEditor.getEditorComponent match {
-      case text: JTextField => text.setColumns(3)
+      case text: JTextField => text.setColumns(4)
       case _ =>
     }