[GitHub][workflows] Ask reviewers to merge PRs when author cannot (#81142)

This uses
https://pygithub.readthedocs.io/en/stable/github_objects/Repository.html?highlight=get_collaborator_permission#github.Repository.Repository.get_collaborator_permission.

Which does
https://docs.github.com/en/rest/collaborators/collaborators?apiVersion=2022-11-28#get-repository-permissions-for-a-user
and returns the top level "permission" key.

This is less detailed than the user/permissions key but should be fine
for this
use case.

When a review is submitted we check:
* If it's an approval.
* Whether we have already left a merge on behalf comment (by looking for
a hidden HTML comment).
* Whether the author has permissions to merge their own PR. 
* Whether the reviewer has permissions to merge.

If needed we leave a comment tagging the reviewer. If the reviewer also
doesn't have merge permission, then it asks them to find someone else
who does.

0 files changed, 0 insertions, 0 deletions