diff options
-rw-r--r-- | Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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 |