diff options
| author | bjorn <bjorn@bringert.net> | 2008-08-18 20:22:25 +0000 |
|---|---|---|
| committer | bjorn <bjorn@bringert.net> | 2008-08-18 20:22:25 +0000 |
| commit | 401d1cd7d10b5e1596d4dc82f926a8feb1d6e3ea (patch) | |
| tree | cbe5d4e532f78ff080efb6452e148c3974819eb4 /examples/peacekeeping/PeaceSyntaxI.gf | |
| parent | 256ab548070e360bbd8b395c56ea4ce51cf0f339 (diff) | |
Some peacekeeping clean-up, still far from compiling.
Diffstat (limited to 'examples/peacekeeping/PeaceSyntaxI.gf')
| -rw-r--r-- | examples/peacekeeping/PeaceSyntaxI.gf | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/examples/peacekeeping/PeaceSyntaxI.gf b/examples/peacekeeping/PeaceSyntaxI.gf index 89517d735..9f29f9f3c 100644 --- a/examples/peacekeeping/PeaceSyntaxI.gf +++ b/examples/peacekeeping/PeaceSyntaxI.gf @@ -2,8 +2,6 @@ incomplete concrete PeaceSyntaxI of PeaceSyntax = PeaceCatI ** open Lang,PeaceRes in { flags --- optimize = all_subs ; - optimize = share ; unlexer = text ; lexer = text ; lincat |