summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRobert Norton2018-04-26 11:49:00 +0100
committerRobert Norton2018-04-26 11:49:57 +0100
commitdf13578f590badfb73fb3c62e045af15fa1a9573 (patch)
tree1ded4993af0b48b5f188ad2cdee487b674ccec02
parent1bd54ce4c7d85b150f2200abeed0dff67087837c (diff)
Fix apply_header target with location of LICENSE file.
-rw-r--r--Makefile8
1 files changed, 4 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index a343e257..71a08f64 100644
--- a/Makefile
+++ b/Makefile
@@ -43,10 +43,10 @@ apply_header:
$(MAKE) clean
headache -c etc/headache_config -h etc/mips_header `ls mips/*.sail`
headache -c etc/headache_config -h etc/mips_header `ls cheri/*.sail`
- headache -c etc/headache_config -h src/LICENCE `ls src/Makefile*`
- headache -c etc/headache_config -h src/LICENCE `ls src/*.ml*`
- headache -c etc/headache_config -h src/LICENCE `ls src/lem_interp/*.ml`
- headache -c etc/headache_config -h src/LICENCE `ls src/lem_interp/*.lem`
+ headache -c etc/headache_config -h LICENCE `ls src/Makefile*`
+ headache -c etc/headache_config -h LICENCE `ls src/*.ml*`
+ headache -c etc/headache_config -h LICENCE `ls src/lem_interp/*.ml`
+ headache -c etc/headache_config -h LICENCE `ls src/lem_interp/*.lem`
$(MAKE) -C arm apply_header
clean: