author | wenzelm |
Sat, 12 Jan 2013 21:15:44 +0100 | |
changeset 50853 | 86389991636e |
parent 50852 | a667ac8c7afe |
child 50854 | 2b15227b17e8 |
--- a/src/Pure/Tools/build_dialog.scala Sat Jan 12 21:12:00 2013 +0100 +++ b/src/Pure/Tools/build_dialog.scala Sat Jan 12 21:15:44 2013 +0100 @@ -75,7 +75,7 @@ /* text */ val text = new TextArea { - font = new Font("SansSerif", Font.PLAIN, Library.resolution_scale(10)) + font = new Font("SansSerif", Font.PLAIN, Library.resolution_scale(10) max 14) editable = false columns = 50 rows = 20