summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorRobert Norton2018-07-09 14:50:16 +0100
committerRobert Norton2018-07-09 14:57:20 +0100
commit8139ae498b4809833394b3e0548757426ff912cc (patch)
treeef6e8bd7985ab1d921b4a74f5b769281e2466b13 /Makefile
parentd829021b5f64d3c6b4ad39c69a5f36475d8e7071 (diff)
Support building an anonymised version of manual. Fix sail example in manual. Remove incomplete types chapter from manual per AA's recommendation.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile11
1 files changed, 11 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index bfbf6bef..9a6dd42a 100644
--- a/Makefile
+++ b/Makefile
@@ -53,6 +53,17 @@ apply_header:
headache -c etc/headache_config -h LICENCE `ls src/lem_interp/*.lem`
$(MAKE) -C arm apply_header
+anon_dist:
+ $(MAKE) clean
+ 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 src/Makefile*`
+ headache -c etc/headache_config -h etc/anon_header `ls src/*.ml*`
+ headache -c etc/headache_config -h etc/anon_header `ls src/lem_interp/*.ml`
+ headache -c etc/headache_config -h etc/anon_header `ls src/lem_interp/*.lem`
+ headache -c etc/headache_config -h etc/anon_header `ls arm/*.sail`
+ tar cvzf sail.tar.gz .
+
clean:
for subdir in src arm ; do\
$(MAKE) -C "$$subdir" clean;\