1 files changed, 0 insertions, 9 deletions
diff --git a/_tags b/_tags
deleted file mode 100644
index 0d83f2fa..00000000
--- a/_tags
+++ /dev/null
@@ -1,9 +0,0 @@
-true: use_menhir
-<**/*.cmx>: debug
-<**/*.native>: debug
-<driver/Driver.*{byte,native}>: use_unix,use_str
-<exportclight/Clightgen.*{byte,native}>: use_unix,use_str
-<checklink/*.ml>: pkg_bitstring
-<checklink/Validator.*{byte,native}>: pkg_unix,pkg_str,pkg_bitstring
-<extraction/*.ml>: warn(-20)
-<**/*.ml>: warn(-3)