Topic: Dependent issues bot
Bryan Gin-ge Chen (Dec 09 2020 at 19:32):
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.
Last updated: May 16 2021 at 05:21 UTC