diff options
author | Son HO | 2024-04-15 16:59:10 +0200 |
---|---|---|
committer | GitHub | 2024-04-15 16:59:10 +0200 |
commit | 2545ad25384156d7d8d798567bc922be798a20e3 (patch) | |
tree | 8c40bb8193267bed4728557d9e8e8ec84810a9d4 | |
parent | 67eaff0b90d693c86d9848cbf598e7c86caba4c4 (diff) | |
parent | 0edc8c924c356052395445cce16fd79ebf468818 (diff) |
Merge pull request #127 from AeneasVerif/fix-ci
Fix CI
-rw-r--r-- | Makefile | 5 | ||||
-rw-r--r-- | flake.nix | 2 |
2 files changed, 5 insertions, 2 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 \ @@ -82,7 +82,7 @@ # files like lakefile.lean, and the user hand-written files) # Run the tests - remark: we could remove the file - make tests -j $NIX_BUILD_CORES + make test-all -j $NIX_BUILD_CORES # Check that there are no differences between the generated tests # and the original tests |