From d8d661d02cf0068753ae3963156896492dfde50a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 28 Oct 2022 17:36:58 +0200
Subject: Update the Makefile

---
 Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Makefile')

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
-- 
cgit v1.2.3