From ad3fd6c08237d4f23af5cd0facf80872222b946f Mon Sep 17 00:00:00 2001
From: janna <unknown>
Date: Fri, 13 Aug 2004 12:16:00 +0000
Subject: [PATCH] *** empty log message ***

---
 src/JavaGUI/GFEditor2.java | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/JavaGUI/GFEditor2.java b/src/JavaGUI/GFEditor2.java
index 12a265741..8ca0c3fc1 100644
--- a/src/JavaGUI/GFEditor2.java
+++ b/src/JavaGUI/GFEditor2.java
@@ -14,7 +14,7 @@ import java.util.*;
 public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
     KeyListener, FocusListener {                        
 
-    private int[] sizes = {16,18,20,25,30,36};
+    private int[] sizes = {14,18,22,26,30};
     private String[] envfonts;
     private Font font;  
     Font[] fontObjs;
@@ -1027,17 +1027,17 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
         font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue());
         //output.setFont(font);  
         fontEveryWhere(font);
-        cbMenuItem.setFont(font);  
-        rbMenuItem.setFont(font);  
-        fileMenuItem.setFont(font);  
+        if (cbMenuItem!=null) cbMenuItem.setFont(font);  
+        if (rbMenuItem!=null) rbMenuItem.setFont(font);  
+        if (fileMenuItem!=null) fileMenuItem.setFont(font);  
     }
 
     if ( obj == sizeList ) {
         font = new Font((String)fontList.getSelectedItem(), Font.PLAIN, ((Integer)sizeList.getSelectedItem()).intValue());
         fontEveryWhere(font);
-        cbMenuItem.setFont(font);  
-        rbMenuItem.setFont(font);  
-        fileMenuItem.setFont(font);  
+        if (cbMenuItem!=null) cbMenuItem.setFont(font);  
+        if (rbMenuItem!=null) rbMenuItem.setFont(font);  
+        if (fileMenuItem!=null) fileMenuItem.setFont(font);  
    }
 
     if ( obj == menu ) {