aboutsummaryrefslogtreecommitdiffhomepage
path: root/CONTRIBUTING.md
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-11 14:58:46 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-14 10:51:18 +0200
commit0fdf916c8c75743e6899ade78366b005c1141bc0 (patch)
tree421fc0783683094a708bb652cea17d480c7dab27 /CONTRIBUTING.md
parent9368a1572f55dea66aa21edf140b84d883c5fccc (diff)
Update CI documentation following recent evolutions.
Diffstat (limited to 'CONTRIBUTING.md')
-rw-r--r--CONTRIBUTING.md8
1 files changed, 7 insertions, 1 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 1a3c99369..7fb976ee0 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -28,7 +28,13 @@ Please make pull requests against the `master` branch.
If it's your first significant contribution to Coq (significant means: more than fixing a typo), your pull request should include a commit adding your name to the [`CREDITS`](/CREDITS) file (possibly with the name of your institution / employer if relevant to your contribution, an ORCID if you have one —you may log into https://orcid.org/ using your institutional account to get one—, and the year of your contribution).
-It's helpful to run the Coq test suite with `make test-suite` before submitting your change. Travis CI runs this test suite and a much larger one including external Coq developments on every pull request, but these results take significantly longer to come back (on the order of a few hours). Running the test suite locally will take somewhere around 10-15 minutes. Refer to [`dev/ci/README.md`](/dev/ci/README.md#information-for-developers) for more information on Travis CI tests.
+It's helpful to run the Coq test suite with `make test-suite` before submitting
+your change. Our CI runs this test suite and lots of other tests, including
+building external Coq developments, on every pull request, but these results
+take significantly longer to come back (on the order of a few hours). Running
+the test suite locally will take somewhere around 10-15 minutes. Refer to
+[`dev/ci/README.md`](/dev/ci/README.md#information-for-developers) for more
+information on CI tests, including how to run them on your private branches.
If your pull request fixes a bug, please consider adding a regression test as well. See [`test-suite/README.md`](/test-suite/README.md) for how to do so.