Document test-suite PRINT_LOGS.

1 files changed, 50 insertions, 0 deletions

diff --git a/test-suite/README.md b/test-suite/README.md
index 1ec5d667e..1d1195646 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -12,6 +12,56 @@ 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 the `test-suite` directory, `make report` (included in `make
+all`) prints a summary of which tests failed using the produced log
+files (this still works when only some tests are built as described
+above). Setting the `PRINT_LOGS` variable will make it print the logs
+of the failing tests.
+
+For instance, running the following in the `test-suite` directory:
+
+```bash
+$ echo Fail. > success/fail.v # make some failing test
+
+$ make
+TEST      prerequisite/make_local.v
+...
+TEST      success/fail.v
+...
+BUILDING SUMMARY FILE
+FAILURES
+    success/fail.v...Error! (should be accepted)
+Makefile:189: recipe for target 'all failed
+make: *** [report] Error 1
+
+$ make report PRINT_LOGS=1
+BUILDING SUMMARY FILE
+logs/success/fail.v.log
+==========> TESTING success/fail.v <==========
+Welcome to Coq (version information)
+Skipping rcfile loading.
+File "/path/to/success/fail.v", line 1, characters 4-5:
+Error:
+Syntax error: [vernac:Vernac.vernac_control] expected after 'Fail' (in [vernac:Vernac.vernac_control]).
+
+0m0.000000s 0m0.000000s
+0m0.040000s 0m0.000000s
+==========> FAILURE <==========
+    success/fail.v...Error! (should be accepted)
+
+FAILURES
+    success/fail.v...Error! (should be accepted)
+Makefile:189: recipe for target 'report' failed
+make: *** [report] Error 1
+
+$ echo 'Comments "foo".' > success/fail.v
+
+$ make
+TEST      success/fail.v
+BUILDING SUMMARY FILE
+NO FAILURES
+```
+
 See [`test-suite/Makefile`](/test-suite/Makefile) for more information.
 
 ## Adding a test