diff options
Diffstat (limited to 'test-suite/README.md')
| -rw-r--r-- | test-suite/README.md | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/test-suite/README.md b/test-suite/README.md index 159697a7e..2e288ff73 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -1,9 +1,18 @@ # Coq Test Suite -The test suite can be run from the root directory by `make test-suite`. +The test suite can be run from the Coq root directory by `make test-suite`. +This does a clean step first, so if you've already run it, then change something, +you'll have to do a lot of work again. + +If you run `make` from the `test-suite` directory, there is no clean step. +You can also run `make aaa/bbb/ccc.v.log` to build the log for one test, +or `make ddd` where `ddd` is on of the sub-directories of `test-suite` +to just build the logs for that directory. +Logs are stored in said `.log` file. +In these cases, a summary is not printed, but can be generated by `make summary`. + +`make -B` can be used to rerun tests ( -B meaning always remake). -From this directory, `make aaa/bbb/ccc.v.log` runs one test (if not already run), storing the output in the named `.log` file. -`make -B` can be used to rerun the test (`-B` meaning always remake). See [`test-suite/Makefile`](/test-suite/Makefile) for more information. ## Adding a test |