Dependent issues bot

Stream: general

[Bryan Gin-ge Chen]

With the merging of #5261, we have a new piece of automation for the mathlib github repo. Please give a warm welcome to dependent-issues bot!

This github action will manage the "blocked-by-other-PR" label and post comments on PRs with dependencies. (Those of us watching the mathlib repo will have already noticed the 20+ new comments on our current open PRs.)

To make use of it, just make sure to include the text - [ ] depends on: #PR_NUMBER in your PR comment (as we have been doing already).

Feel free to post here if you notice any issues.