# 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 _ => }