diff options
| author | Jason Gross | 2018-08-29 11:34:43 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-29 11:35:36 -0400 |
| commit | 7fe8212d42e6dee2d117d15f9acbd4c3decfad13 (patch) | |
| tree | 9fb08c7ae8c6beea85a39867b57fe4c3057d71c2 | |
| parent | 0c6e4e6e3cbf8187cf62bce64fb9b6e06a4036c6 (diff) | |
Move mention of dev/doc/critical-bugs to CONTRIBUTING
As per https://github.com/coq/coq/pull/8349#pullrequestreview-150456919
| -rw-r--r-- | .github/PULL_REQUEST_TEMPLATE.md | 3 | ||||
| -rw-r--r-- | CONTRIBUTING.md | 3 |
2 files changed, 3 insertions, 3 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index f0747134da..4a8606a38a 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -17,6 +17,3 @@ Fixes / closes #???? <!-- (Otherwise, remove these lines.) --> - [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified). - [ ] Entry added in CHANGES. -<!-- If this closes a critical bug (a proof of False): --> -<!-- (Otherwise, remove this line.) --> -- [ ] Corresponding entry in `dev/doc/critical-bugs` was added / updated diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index cd4a246bb4..de7fb9183c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -50,6 +50,9 @@ 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. +If your pull request fixes a critical bug (a bug allowing a proof of `False`), +please add an entry to [`dev/doc/critical-bugs`](/dev/doc/critical-bugs). + 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. Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by Travis (using `git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`. |