aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-10-08 23:00:40 +0100
committerYann Herklotz <git@yannherklotz.com>2021-10-08 23:00:40 +0100
commit0a7eca06548e7261e28ba49679cc2ba4e6851e59 (patch)
tree0f050c71616d047074b8b482339edb3270194e27 /Makefile
parent82604915aab691007abfa937fd5e90d646332034 (diff)
downloadvericert-0a7eca06548e7261e28ba49679cc2ba4e6851e59.tar.gz
vericert-0a7eca06548e7261e28ba49679cc2ba4e6851e59.zip
Fix running of tests using a Makefile
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index d14ef13..0749d1c 100644
--- a/Makefile
+++ b/Makefile
@@ -54,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"
@@ -73,6 +73,7 @@ Makefile.coq:
clean:: Makefile.coq
$(MAKE) -f Makefile.coq clean
+ $(MAKE) -C test clean
rm -f Makefile.coq
clean::