Sync labels with GitHub states by a bot

[seb....@gmail.com]

Hello everyone,


More than a month has passed since we migrated to GitHub. As you explored the new workflows, you may have noticed that there are some redundancies regarding a PR's status. On the one hand there are states supported by GitHub to mark a PR as draft or approved... on the other hand there are labels migrated from Trac that show almost the same thing (s: need review, s : positive_review . ..).

The need to have them in parallel was discussed in issues 8 of the trac-to-github repo (see this comment there). To simplify our manual workflows and keep the redundant labels reliable, I implemented a bot to sync these labels with their corresponding GitHub states. Please take a look at PR #35172.

Best
Sebastian

[Kwankyu Lee]

Thanks a lot!