diff options
Diffstat (limited to 'src/JavaGUI')
| -rw-r--r-- | src/JavaGUI/GFEditor2.java | 2 |
1 files changed, 1 insertions, 1 deletions
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);
|