aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
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