aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 5 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 763c892..0749d1c 100644
--- a/Makefile
+++ b/Makefile
@@ -31,8 +31,10 @@ all: lib/COMPCERTSTAMP
$(MAKE) proof
$(MAKE) compile
-lib/COMPCERTSTAMP:
+lib/CompCert/Makefile.config: lib/CompCert/configure
(cd lib/CompCert && ./configure --ignore-coq-version $(ARCH))
+
+lib/COMPCERTSTAMP: lib/CompCert/Makefile.config
$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/CompCert
touch $@
@@ -52,7 +54,7 @@ doc: Makefile.coq
extraction: src/extraction/STAMP
test:
- ./test/test_all.sh ./test
+ $(MAKE) -C test
compile: src/extraction/STAMP
@echo "OCaml bin/vericert"
@@ -71,6 +73,7 @@ Makefile.coq:
clean:: Makefile.coq
$(MAKE) -f Makefile.coq clean
+ $(MAKE) -C test clean
rm -f Makefile.coq
clean::