diff options
Diffstat (limited to 'dev/ci/README.md')
| -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 f4423558c..bb13587e9 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 --------------------------- |