Manage GH labels using the new 'labels' tool

2018-07-14 10:09:22 -03:00
parent 0565a7a4e1
commit 35ffd29404
2 changed files with 154 additions and 0 deletions
--- a/doc/en/development_guide.rst
+++ b/doc/en/development_guide.rst
@@ -39,6 +39,11 @@ avoid creating labels just for the sake of creating them.

 Each label should include a description in the GitHub's interface stating its purpose.

+Labels are managed using `labels <https://github.com/hackebrot/labels>`_. All the labels in the repository
+are kept in ``.github/labels.toml``, so any changes should be via PRs to that file.
+After a PR is accepted and merged, one of the maintainers must manually synchronize the labels file with the
+GitHub repository.
+
 Temporary labels
 ~~~~~~~~~~~~~~~~