diff options
| author | Nadrieril | 2024-04-15 16:05:48 +0200 |
|---|---|---|
| committer | Nadrieril | 2024-04-15 16:05:48 +0200 |
| commit | 0edc8c924c356052395445cce16fd79ebf468818 (patch) | |
| tree | 8c40bb8193267bed4728557d9e8e8ec84810a9d4 /Makefile | |
| parent | 67eaff0b90d693c86d9848cbf598e7c86caba4c4 (diff) | |
Fix CI
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -89,7 +89,10 @@ clean: # Test the project by translating test files to F* .PHONY: test -test: build-dev test-no_nested_borrows test-paper \ +test: build-dev test-all + +.PHONY: test-all +test-all: test-no_nested_borrows test-paper \ test-hashmap test-hashmap_main \ test-external test-constants \ testp-polonius_list testp-betree_main \ |