From 2e0b408b69d40ab457c998854e43d0b60dd1c68b Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Wed, 10 Jan 2018 12:39:09 +0900 Subject: Add comments by @psteckler to test-suite/README.md --- test-suite/README.md | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'test-suite/README.md') 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 -- cgit v1.2.3