diff options
| author | Brian Campbell | 2017-08-10 16:57:04 +0100 |
|---|---|---|
| committer | Brian Campbell | 2017-08-10 16:57:04 +0100 |
| commit | 41b3f6a2f45c6ee24e7db8b65a4df81f9eb2aca0 (patch) | |
| tree | 2163b19147ec09e66c0d5bdc39a6bfc5352805f7 /src | |
| parent | 5c01bf4c78860b1173b156f99d03f115d08e2175 (diff) | |
Disable menhir on this branch
(until location information is updated)
Diffstat (limited to 'src')
| -rw-r--r-- | src/_tags | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -1,4 +1,5 @@ -true: -traverse, debug, use_menhir +true: -traverse, debug +#, use_menhir <**/*.ml>: bin_annot, annot <lem_interp> or <test>: include <sail.{byte,native}>: use_pprint, use_nums, use_unix |
