Skip to content
Snippets Groups Projects
Commit aa23528c authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'document-makefile-options' into 'master'

Document Makefile flags NO_TEST and MAKE_REF together

See merge request iris/iris!500
parents b28c9929 0c06c06d
No related branches found
No related tags found
No related merge requests found
......@@ -46,6 +46,8 @@ Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
Coq-8.8-specific `.ref` file). If you change one of these, remember to update
*all* the `.ref` files.
If you want to compile without tests run `make NO_TEST=1`.
## How to measure the timing effect on a reverse dependency
So say you did a change in Iris, and want to know how it affects [lambda-rust]
......
# use NO_TEST=1 to skip the tests
NO_TEST:=
# use MAKE_REF=1 to generate new reference files
MAKE_REF:=
# Run tests interleaved with main build. They have to be in the same target for this.
real-all: $(if $(NO_TEST),,test)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment