summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorJon French2018-12-28 15:12:00 +0000
committerJon French2018-12-28 15:12:00 +0000
commitb59fba68e535f39b6285ec7f4f693107b6e34148 (patch)
tree3135513ac4b23f96b41f3d521990f1ce91206c99 /Makefile
parent9f6a95882e1d3d057bcb83d098ba1b63925a4d1f (diff)
parent2c887e7d01331d3165120695594eac7a2650ec03 (diff)
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 0 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 40040a11..12684d91 100644
--- a/Makefile
+++ b/Makefile
@@ -56,8 +56,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*`