Skip to content

Commit

Permalink
Change the tests target to test
Browse files Browse the repository at this point in the history
  • Loading branch information
sonmarcho committed Mar 11, 2024
1 parent 74dcc7a commit 7875ac6
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 6 deletions.
4 changes: 2 additions & 2 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -88,8 +88,8 @@ clean:
cd compiler && dune clean

# Test the project by translating test files to F*
.PHONY: tests
tests: test-no_nested_borrows test-paper \
.PHONY: test
test: test-no_nested_borrows test-paper \
test-hashmap test-hashmap_main \
test-external test-constants \
testp-polonius_list testp-betree_main \
Expand Down
8 changes: 4 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -60,11 +60,11 @@ if [ -e charon ]; then echo "valid"; else echo "invalid"; fi
Finally, building the project simply requires to run `make` in the top
directory.

You can also use `make tests` and `make verify` to run the tests, and check
the generated files. As `make tests` will run tests which use the Charon tests,
You can also use `make test` and `make verify` to run the tests, and check
the generated files. As `make test` will run tests which use the Charon tests,
you will need to regenerate the `.llbc` files. You have the following options:
- run `make tests` in the Charon repository
- run `REGEN_LLBC=1 make tests` in the Aeneas repository
- run `make test` in the Charon repository
- run `REGEN_LLBC=1 make test` in the Aeneas repository

## Documentation

Expand Down

0 comments on commit 7875ac6

Please sign in to comment.