diff options
| author | Maxime Dénès | 2018-01-11 18:18:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-11 18:18:15 +0100 |
| commit | 3815ec5405976196ff79b6960e65ce5adda66205 (patch) | |
| tree | a9db7c4259f79a364cb15e41363a4d9fd11c2aad /dev | |
| parent | 2202808309a6b307d327fd7c76da55b466166864 (diff) | |
| parent | 25f910c9229218e08b1a4bbfa22c02fa43bb2394 (diff) | |
Merge PR #6557: First stab at documenting the test suite.
Diffstat (limited to 'dev')
| -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 --------------------------- |