Zulip Chat Archive
Stream: general
Topic: PR titles in bors batch
Damiano Testa (Aug 27 2023 at 07:43):
Looking at the current Bors queue, displays just the PR number. Would it be easy to display the PR title?
Damiano Testa (Aug 27 2023 at 07:46):
(With bors going away soon, this only makes sense if it is easy and quick)
Last updated: Dec 20 2023 at 11:08 UTC