diff options
| author | Peter Sewell | 2013-06-22 13:45:30 +0100 |
|---|---|---|
| committer | Peter Sewell | 2013-06-22 13:45:30 +0100 |
| commit | 32bb8d65ce4258a085bb676a2e0e675be621cf6e (patch) | |
| tree | 47b44c9ca3eafbe02535bcb4fcd8bdb176bbd12c /language/Makefile | |
| parent | a3014afbbf493dc2cdc6fc4fb938602c476b5991 (diff) | |
use new Ott aux hom to auto-generate location-annotated rules (to reduce
the noise). More harmonisation of location annotation for identifiers
and of production-name prefixes still needed.
Diffstat (limited to 'language/Makefile')
| -rw-r--r-- | language/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/language/Makefile b/language/Makefile index 6576e3d8..f8858e31 100644 --- a/language/Makefile +++ b/language/Makefile @@ -10,7 +10,8 @@ l2Theory.uo: l2Script.sml Holmake --qof -I $(OTTLIB) l2Theory.uo l2.tex ../src/ast.ml l2Script.sml: l2.ott - ott -ocaml_include_terminals true -o l2.tex -o l2.ml -o l2Script.sml -picky_multiple_parses true l2.ott + ott -sort false -generate_aux_rules false -o l2.tex -picky_multiple_parses true l2.ott + ott -sort false -generate_aux_rules true -ocaml_include_terminals true -o l2.ml -o l2Script.sml -picky_multiple_parses true l2.ott #rm -f ../src/ast.ml # chmod a-w ../src/ast.ml |