aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-04-02 14:54:05 +0100
committerYann Herklotz <git@yannherklotz.com>2020-04-02 14:54:05 +0100
commit5398b08ec6d445f91ed74c8434150cfbf99cc373 (patch)
treee65b87037f644b68c65aa1b971bd0085c80b6eda /Makefile
parent7a76e9d632756a4d3f044d6742a5defb83ce6ae7 (diff)
downloadvericert-5398b08ec6d445f91ed74c8434150cfbf99cc373.tar.gz
vericert-5398b08ec6d445f91ed74c8434150cfbf99cc373.zip
Update makefile for tests
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 4 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 3c62851..0c26d57 100644
--- a/Makefile
+++ b/Makefile
@@ -16,7 +16,7 @@ VS := src/Compiler.v $(VSSUBDIR)
PREFIX ?= .
-.PHONY: all install proof clean extraction
+.PHONY: all install proof clean extraction test
all: lib/COMPCERTSTAMP
$(MAKE) proof
@@ -38,6 +38,9 @@ proof: Makefile.coq
extraction: src/extraction/STAMP
+test:
+ ./test/test_all.sh ./test
+
compile: src/extraction/STAMP
@echo "OCaml bin/coqup"
@mkdir -p bin