mathlib

81d8104f - feat(actions): manage labels on PR review (#2387)

feat(actions): manage labels on PR review (#2387) Github actions will now add "ready-to-merge" to PRs that are approved by writing "bors r+" / "bors merge" in a PR reviews. It will also remove the "request-review" label, if present.