diff options
| author | Son Ho | 2022-10-28 17:36:58 +0200 |
|---|---|---|
| committer | Son HO | 2022-10-28 17:41:04 +0200 |
| commit | d8d661d02cf0068753ae3963156896492dfde50a (patch) | |
| tree | 11e829f43594d3e180dd0405a2ca1e3103dd50da | |
| parent | 13ed942e1f29577a155991c7c313aad38637615a (diff) | |
Update the Makefile
| -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 |