summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorAlasdair2019-01-14 10:36:43 +0000
committerAlasdair2019-01-14 10:36:43 +0000
commit2eb2566c5c3ef5d7250fea604933704d8d94eabe (patch)
tree8bebb52a23c3982514b769beffac82e8ac06cd6c /Makefile
parent9cfa575245a0427a0d35504086de182bd80b7df8 (diff)
parenta3da2efb3ef08e132e16db0c510b1b8fe4ee600c (diff)
Merge remote-tracking branch 'origin/sail2' into asl_flow2
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 0 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 6ce13857..cee5c3c6 100644
--- a/Makefile
+++ b/Makefile
@@ -60,8 +60,6 @@ apply_header:
anon_dist:
headache -c etc/headache_config -h etc/anon_header `ls mips/*.sail`
headache -c etc/headache_config -h etc/anon_header `ls cheri/*.sail`
- headache -c etc/headache_config -h etc/anon_header `ls riscv/*.sail`
- headache -c etc/headache_config -h etc/anon_header `ls riscv/*.ml`
headache -c etc/headache_config -h etc/anon_header `ls lib/*.ml`
headache -c etc/headache_config -h etc/anon_header `ls lib/coq/*.v`
headache -c etc/headache_config -h etc/anon_header `ls src/Makefile*`