author | wenzelm |
Tue, 06 May 2014 23:35:24 +0200 | |
changeset 56888 | 3e8cbb624cc5 |
parent 56887 | 1ca814da47ae |
child 56889 | 48a745e1bde7 |
child 56890 | 7f120d227ca5 |
--- 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 _ => }