diff options
| author | Jasper Hugunin | 2018-01-06 21:40:02 +0900 |
|---|---|---|
| committer | Jasper Hugunin | 2018-01-06 21:40:02 +0900 |
| commit | 8c1aa693f718414bba8cd1400d2b49ff39eeb828 (patch) | |
| tree | ceaaf7e097d93e8410e487a904cc5d6d5fba7bae /dev/ci | |
| parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) | |
First stab at documenting the test suite.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/README.md | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index f4423558cc..bb13587e94 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -103,6 +103,8 @@ The process to merge your PR is then to submit PRs to the external development repositories, merge the latter first (if the fixes are backward-compatible), drop the overlay commit and merge the PR on Coq then. +See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. + Travis specific information --------------------------- |