Use GH labels, save time



Lots of GitHub issues and PRs are being created daily.

To help us manage them we have “labels”: to classify them by area, type, priority, or to mark them in need of attention.


When creating a GitHub issue or pull request, remember to add the appropriate labels.

It takes a couple of seconds.

If you are reviewing a PR, and there is missing or incorrect labels, fix it *

This will save us all time when searching,

reduce the chances of your PR/issue being forgotten,

speed up reviewing,

reduce the changes of duplicates, etc.


Best regards,

Alberto Escolar Piedras


*(1st time contributors cannot add labels)

Join to automatically receive all group messages.