Zulip Chat Archive

Stream: general

Topic: Dependent issues bot

Bryan Gin-ge Chen (Dec 09 2020 at 19:32):

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.

Last updated: Dec 20 2023 at 11:08 UTC