diff options
| author | Théo Zimmermann | 2018-08-30 10:00:01 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-30 10:00:01 +0200 |
| commit | bc4611f372a50cae3e2e466bb1caf09bfa659e2e (patch) | |
| tree | 345d60d22a4403c179c2a39d4756e60e79e0a3f6 | |
| parent | 0745b31e986b79692e4e282877555963d0f26a8f (diff) | |
| parent | 7fe8212d42e6dee2d117d15f9acbd4c3decfad13 (diff) | |
Merge PR #8349: Mention dev/doc/critical-bugs in CONTRIBUTING
| -rw-r--r-- | CONTRIBUTING.md | 3 |
1 files changed, 3 insertions, 0 deletions
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`. |