From fe3def270fd0f601cdccfa4c5f443cee028c3f03 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 13 Feb 2019 17:49:49 +0100
Subject: Document how to add people to the contributors team.

---
 CONTRIBUTING.md | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'CONTRIBUTING.md')

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)** \
-- 
cgit v1.2.3