aboutsummaryrefslogtreecommitdiffstats
path: root/_tags
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2014-11-22 14:28:52 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2014-11-22 14:28:52 +0100
commit0c80820c3850fa2b0713f7519c7085e949cc7cb2 (patch)
treea579eef3d12dd41be15fadf74b18d5fbd90e7a8f /_tags
parent84116d49db9d485e468e6902df801c7be8ed2ffe (diff)
downloadcompcert-0c80820c3850fa2b0713f7519c7085e949cc7cb2.tar.gz
compcert-0c80820c3850fa2b0713f7519c7085e949cc7cb2.zip
Remove ocamlbuild configuration files, no longer used.
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)