From 310ba62601ebb9953bae379ea53f9c6ada163821 Mon Sep 17 00:00:00 2001
From: janna <unknown>
Date: Wed, 22 Dec 2004 14:47:06 +0000
Subject: [PATCH] *** empty log message ***

---
 src/JavaGUI/GFEditor2.java | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/JavaGUI/GFEditor2.java b/src/JavaGUI/GFEditor2.java
index d093fcf38..0968b6236 100644
--- a/src/JavaGUI/GFEditor2.java
+++ b/src/JavaGUI/GFEditor2.java
@@ -667,7 +667,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
         linearization += result+"\n";           
         result = fromProc.readLine();
         if (debug) System.out.println("6 "+result);
-        while (result.indexOf("/linearization")==-1){       
+        while ((result!=null)&&(result.indexOf("/linearization")==-1)){       
           linearization += result+"\n";           
           result = fromProc.readLine();
           if (debug) System.out.println("6 "+result);