Zulip Chat Archive
Stream: general
Topic: triage bot
Mario Carneiro (Jul 29 2023 at 06:13):
Who is running the #triage bot? And can we get it to run on mathlib4 issues?
Mario Carneiro (Jul 29 2023 at 06:14):
perhaps it should select from a pool of both mathlib and mathlib4 issues, possibly excluding too-late mathlib PRs
Eric Wieser (Jul 29 2023 at 07:26):
It's being run by GitHub, from the azure-scripts repo
Last updated: Dec 20 2023 at 11:08 UTC