Wolfgang Walther 1e6124a504 ci/github-script/merge: list eligible users in comment ...

When a user tries to merge a PR, but is not allowed to, it is helpful to
explicitly list the users who *are* allowed. This helps explaining *why*
the merge-eligible label was set.

I objected to this proposal before, because it would incur too many API
requests. But after we have restructured the checklist, this is not
actually true anymore - we can now sensibly run this only when a comment
is posted and not whenever we check a PR for eligibility.

2025-11-04 20:50:41 +01:00

9.7 KiB

Raw Blame History

View Raw