summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 7d295974..c9b0b566 100644
--- a/Makefile
+++ b/Makefile
@@ -94,11 +94,11 @@ trans-polonius-betree_main: SUBDIR:=betree
# vary with the test files.
.PHONY: gen-llbc-polonius-%
gen-llbc-polonius-%: build
- cd $(CHARON_HOME)/tests-polonius && $(MAKE) test-$*
+ cd $(CHARON_HOME)/tests-polonius && NOT_ALL_TESTS=1 $(MAKE) test-$*
.PHONY: gen-llbc-%
gen-llbc-%: build
- cd $(CHARON_HOME)/tests && $(MAKE) test-$*
+ cd $(CHARON_HOME)/tests && NOT_ALL_TESTS=1 $(MAKE) test-$*
# Generic rule to test the translation of an LLBC file.
# Note that the files requiring the Polonius borrow-checker are generated