diff options
| author | janna <unknown> | 2004-12-22 14:47:06 +0000 |
|---|---|---|
| committer | janna <unknown> | 2004-12-22 14:47:06 +0000 |
| commit | 310ba62601ebb9953bae379ea53f9c6ada163821 (patch) | |
| tree | eb6b284a3c7f4fae13c8a0a25b3523de47ffb8b6 /src/JavaGUI/GFEditor2.java | |
| parent | 49e901ec653f34183ec3263b950f79f4e54a8a71 (diff) | |
*** empty log message ***
Diffstat (limited to 'src/JavaGUI/GFEditor2.java')
| -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);
|