mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-23 12:52:15 +03:00
Add instructions on how to run a subset of the tests
This commit is contained in:
parent
54f00e9247
commit
e82a0c6acb
2
Makefile
2
Makefile
@ -40,7 +40,7 @@ clean-libs:
|
|||||||
|
|
||||||
test:
|
test:
|
||||||
idris --build tests.ipkg
|
idris --build tests.ipkg
|
||||||
make -C tests only=$(only)
|
@make -C tests only=$(only)
|
||||||
|
|
||||||
install: all install-exec install-libs
|
install: all install-exec install-libs
|
||||||
|
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
IDRIS2 = ../../../idris2
|
IDRIS2 = ../../../idris2
|
||||||
|
|
||||||
test:
|
test:
|
||||||
../runtests $(IDRIS2) --only $(only)
|
@../runtests $(IDRIS2) --only $(only)
|
||||||
|
|
||||||
clean:
|
clean:
|
||||||
find . -name '*.ibc' | xargs rm -f
|
find . -name '*.ibc' | xargs rm -f
|
||||||
|
13
tests/README.md
Normal file
13
tests/README.md
Normal file
@ -0,0 +1,13 @@
|
|||||||
|
Tests
|
||||||
|
=====
|
||||||
|
|
||||||
|
*Note: The commands listed in this section should be run from the repository's root folder.*
|
||||||
|
|
||||||
|
Run all tests: `make test`
|
||||||
|
|
||||||
|
To run only a subset of the tests use: `make test only=NAME`. `NAME` is matched against the path to each test case.
|
||||||
|
|
||||||
|
Examples:
|
||||||
|
- `make test only=chez` will run all Chez Scheme tests.
|
||||||
|
- `make test only=ttimp/basic` will run all basic tests for `TTImp`.
|
||||||
|
- `make test only=idris2/basic001` will run a specific test.
|
Loading…
Reference in New Issue
Block a user