RFR: 1663: Mark integrated Pull Requests as properly merged in their repositories [v57]

[Julian Waters]

On Thu, 5 Jan 2023 18:11:29 GMT, Erik Joelsson <erikj at openjdk.org> wrote:

> I can't say if there is anything in particular that the GitHub API of today is missing that would hinder us from using it for squash merging PRs, at least not without spending a considerable amount of time investigating.

>From my time experimenting with the APIs of both hosts, the only thing really missing is the ability to set the committer and author of the actual Pull Request, like we currently do in `CheckablePullRequest`. Otherwise quite a lot of the existing logic could (with substantial effort) be migrated to use the Pull Request API instead of the current strategy of creating a commit on our own local repositories before pushing to remote ("commit_title" and "commit_message" can already be set from the API for instance, same with GitLab). A rather extreme option to circumvent this issue if we really wanted to utilize the host's merging abilities as altrisi suggests would be giving Skara the ability to force the Pull Request itself (the branch that contains its commits in essence) to allow edits from the pr bot (both GitHub and GitLab support doing so) and pushing the commit from our own local repo into the PR instead, before then merging it through the API as if from the UI as per normal

-------------

PR: https://git.openjdk.org/skara/pull/1409