diff options
| author | Théo Zimmermann | 2019-02-13 17:49:49 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-13 17:49:49 +0100 |
| commit | fe3def270fd0f601cdccfa4c5f443cee028c3f03 (patch) | |
| tree | e96ab0485c977f567d3d1c3cbd88dc2903f0d02c | |
| parent | 315f417e1338473d4d1ff13f49bb0e44c5049544 (diff) | |
Document how to add people to the contributors team.
| -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)** \ |