aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-03-31 19:40:21 +0100
committerYann Herklotz <git@yannherklotz.com>2020-03-31 19:40:21 +0100
commit0b4808a3705317c96387de036381e4e6add4e956 (patch)
tree3da3067ebee6ca85d68fc2c7c0d8b87d9eb18082 /Makefile
parent580cfdf676931f8b590f6f1eb84e42da17569393 (diff)
downloadvericert-0b4808a3705317c96387de036381e4e6add4e956.tar.gz
vericert-0b4808a3705317c96387de036381e4e6add4e956.zip
Add documentation and fix makefile for Compcert
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 6 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 1b4e39b..3c62851 100644
--- a/Makefile
+++ b/Makefile
@@ -18,10 +18,15 @@ PREFIX ?= .
.PHONY: all install proof clean extraction
-all:
+all: lib/COMPCERTSTAMP
$(MAKE) proof
$(MAKE) compile
+lib/COMPCERTSTAMP:
+ (cd lib/CompCert && ./configure x86_64-linux)
+ $(MAKE) -C lib/CompCert
+ touch $@
+
install:
install -d $(PREFIX)/bin
install -C _build/default/driver/compcert.ini $(PREFIX)/bin/.