From a5da3f327f162e31ca21c1f99cf526ca7a583ae2 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Sun, 31 Jan 2010 14:55:07 +0000 Subject: [PATCH] use MrEd:default-font-size preference svn: r17914 --- collects/mred/private/wxme/style.ss | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/collects/mred/private/wxme/style.ss b/collects/mred/private/wxme/style.ss index 8bb830a326..092951786d 100644 --- a/collects/mred/private/wxme/style.ss +++ b/collects/mred/private/wxme/style.ss @@ -1,5 +1,6 @@ #lang scheme/base (require scheme/class + scheme/file (for-syntax scheme/base) "../syntax.ss" "cycle.ss" @@ -18,9 +19,10 @@ write-styles-to-file) (define default-size - (case (system-type) - [(windows) 10] - [else 12])) + (or (get-preference 'MrEd:default-font-size) + (case (system-type) + [(windows) 10] + [else 12]))) (define black-color (make-object color% 0 0 0))