summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/_tags2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/_tags b/src/_tags
index 83ca12e0..d8653781 100644
--- a/src/_tags
+++ b/src/_tags
@@ -1,4 +1,4 @@
-true: -traverse, debug
+true: -traverse, debug, use_menhir
<**/*.ml>: bin_annot, annot
<lem_interp> or <test>: include
<sail.{byte,native}>: use_pprint, use_nums, use_unix