diff options
| author | Wolfgang Walther <walther@technowledgy.de> | 2025-11-04 11:21:14 +0100 |
|---|---|---|
| committer | Wolfgang Walther <walther@technowledgy.de> | 2025-11-04 20:50:41 +0100 |
| commit | 1e6124a504ea2d4ba01039968b00ae670fde3b07 (patch) | |
| tree | 4436c94482a2188280a46f61222c7e7c1bbeb9ea /pkgs/development/python-modules/rangehttpserver | |
| parent | 58a1fe4761b55e98d6652e04fa628d81d3e75a1d (diff) | |
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.
Diffstat (limited to 'pkgs/development/python-modules/rangehttpserver')
0 files changed, 0 insertions, 0 deletions