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 adbeebf12..2751c1c18 100644 --- a/src/JavaGUI/GFEditor2.java +++ b/src/JavaGUI/GFEditor2.java @@ -66,7 +66,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, "erase", "take100", "text", "code", "latexfile",
"structured", "unstructured" };
private String [] modifyMenu = {"Modify", "identity","transfer",
- "compute", "paraphrase", "typecheck", "solve", "context" };
+ "compute", "paraphrase", "generate","typecheck", "solve", "context" };
// private String [] modeMenu = {"Menus", "printname",
// "plain", "short", "long", "typed", "untyped" };
private static String [] newMenu = {"New"};
|