diff options
| author | aarne <unknown> | 2004-05-02 08:21:25 +0000 |
|---|---|---|
| committer | aarne <unknown> | 2004-05-02 08:21:25 +0000 |
| commit | 54947d3e4c7bdcbfa3e00a8eb17c7f0b9696664a (patch) | |
| tree | 8691f24c809b10b047f552690576bb9a6ace9c7c /src/JavaGUI/GFEditor2.java | |
| parent | 487571a685382922f04985995d0f8779284bdc8d (diff) | |
gt Term
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 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"};
|