Add comments by @psteckler to test-suite/README.md

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