From 0a7eca06548e7261e28ba49679cc2ba4e6851e59 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 8 Oct 2021 23:00:40 +0100 Subject: Fix running of tests using a Makefile --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Makefile') 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:: -- cgit