summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorBrian Campbell2017-08-10 16:57:04 +0100
committerBrian Campbell2017-08-10 16:57:04 +0100
commit41b3f6a2f45c6ee24e7db8b65a4df81f9eb2aca0 (patch)
tree2163b19147ec09e66c0d5bdc39a6bfc5352805f7 /src
parent5c01bf4c78860b1173b156f99d03f115d08e2175 (diff)
Disable menhir on this branch
(until location information is updated)
Diffstat (limited to 'src')
-rw-r--r--src/_tags3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/_tags b/src/_tags
index d8653781..a89796b8 100644
--- a/src/_tags
+++ b/src/_tags
@@ -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