aboutsummaryrefslogtreecommitdiffstats
path: root/_tags
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-01-12 14:20:31 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-01-12 14:20:31 +0100
commit81e91f965e7b1afbea8d1630015e75f11f0a3afd (patch)
tree270a85299f33d783e33745c917796f080f7300e1 /_tags
parent3304820b870e4524c7d1f14fcd62506634f7922b (diff)
parent06841a5bb7ca27bc436e87e7991d0d05dbf5267c (diff)
downloadcompcert-81e91f965e7b1afbea8d1630015e75f11f0a3afd.tar.gz
compcert-81e91f965e7b1afbea8d1630015e75f11f0a3afd.zip
Merge branch 'master' into dwarf
Conflicts: powerpc/PrintAsm.ml
Diffstat (limited to '_tags')
-rw-r--r--_tags9
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)