diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-24 09:33:24 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-24 09:33:24 +0100 |
| commit | e3124e098ef8170dac2b348b91757a7034bc4999 (patch) | |
| tree | ce032bbe21d06f2042dc364f381d34d04e4bf4bb /CONTRIBUTING.md | |
| parent | bd41af496fd09d6ecd965190cad2873f1cd6b029 (diff) | |
| parent | 31af3352b0faf2928b6dd0b58530a4332eccf7a8 (diff) | |
Merge PR #6543: Update headers and credits
Diffstat (limited to 'CONTRIBUTING.md')
| -rw-r--r-- | CONTRIBUTING.md | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 74a138f14..213b87735 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -26,6 +26,8 @@ Documentation for getting started with the Coq sources is located in various fil 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. 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. |