lower bound to font size for the sake of Mac OS X (cf. 4cd2d090be8f);
authorwenzelm
Sat, 12 Jan 2013 21:15:44 +0100
changeset 50853 86389991636e
parent 50852 a667ac8c7afe
child 50854 2b15227b17e8
lower bound to font size for the sake of Mac OS X (cf. 4cd2d090be8f);
src/Pure/Tools/build_dialog.scala
--- 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