diff options
| -rw-r--r-- | CONTRIBUTING.md | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 3a8d469a05..cc3af05845 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -43,6 +43,13 @@ extra credit, then you can use the [Coq bug minimizer](https://github.com/JasonGross/coq-tools) (specifically, the bug minimizer is the `find-bug.py` script in that repo). +### Triaging bug reports + +Triaging bug reports (adding labels, closing outdated / resolved bugs) +requires to be granted some permissions. You may request members of the +**@coq/core** team to add you to the contributors team. They can do so using +this link: <https://github.com/orgs/coq/teams/contributors/members?add=true>. + ## Pull requests **Beginner's guide to hacking Coq: [`dev/doc/README.md`](dev/doc/README.md)** \ |