mathlib3

698d6b76 - ci(.github/workflows/dependent-issues.yml): automation for "blocked-by-other-PR" label (#5261)

ci(.github/workflows/dependent-issues.yml): automation for "blocked-by-other-PR" label (#5261) When a PR or issue is updated, the [dependent-issues](https://github.com/z0al/dependent-issues) action will do the following on all PRs which are marked as dependent on it (with the text `- [ ] depends on: #blah` that we're already using): - add / remove the "blocked-by-other-PR" label - post / edit a comment with the current status of its dependencies (this is slightly redundant, given that we have another action which checks off the dependent PRs in the PR comments, but the extra notifications might be useful). - it also adds a new status check which is pending (yellow) until all dependencies are closed.