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);