From 8c1aa693f718414bba8cd1400d2b49ff39eeb828 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 6 Jan 2018 21:40:02 +0900
Subject: First stab at documenting the test suite.

---
 dev/ci/README.md | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev')

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
 ---------------------------
-- 
cgit v1.2.3