diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-01-06 21:40:02 +0900 |
|---|---|---|
| committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-01-06 21:40:02 +0900 |
| commit | 8c1aa693f718414bba8cd1400d2b49ff39eeb828 (patch) | |
| tree | ceaaf7e097d93e8410e487a904cc5d6d5fba7bae /CONTRIBUTING.md | |
| parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) | |
First stab at documenting the test suite.
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 37b556c55..1a769333c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -28,6 +28,8 @@ Please make pull requests against the `master` branch. 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. + Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes. Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. |