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 <https://github.com/sagemath/trac-to-github/issues/8> (see this comment there <https://github.com/sagemath/trac-to-github/issues%20/8#issuecomment-1367744734>). 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 <https://github.com/sagemath/sage/pull/35172>. Best Sebastian -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/9460dea8-4a34-4aca-a11e-b5dc0c635443n%40googlegroups.com.
