# HG changeset patch
# User wenzelm
# Date 1358021744 -3600
# Node ID 86389991636e4a79c4f38bb51811b67ed63a5e5b
# Parent  a667ac8c7afee20010fdd81207e662bb8fad1bb0
lower bound to font size for the sake of Mac OS X (cf. 4cd2d090be8f);

diff -r a667ac8c7afe -r 86389991636e 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