diff --git a/ci/github-script/bot.js b/ci/github-script/bot.js index 20b717238996..d14096add651 100644 --- a/ci/github-script/bot.js +++ b/ci/github-script/bot.js @@ -167,49 +167,6 @@ module.exports = async ({ github, context, core, dry }) => { getUser, }) - // When the same change has already been merged to the target branch, a PR will still be - // open and display the same changes - but will not actually have any effect. This causes - // strange CI behavior, because the diff of the merge-commit is empty, no rebuilds will - // be detected, no maintainers pinged. - // We can just check the temporary merge commit, and if it's empty the PR can safely be - // closed - there are no further changes. - // We only do this for PRs, which are non-empty to start with. This avoids closing PRs - // which have been created with an empty commit for notification purposes, for example - // the yearly election notification for voters. - if (pull_request.merge_commit_sha && pull_request.changed_files > 0) { - const commit = ( - await github.rest.repos.getCommit({ - ...context.repo, - ref: pull_request.merge_commit_sha, - }) - ).data - - if (commit.files.length === 0) { - const body = [ - `The diff for the temporary merge commit ${pull_request.merge_commit_sha} is empty.`, - 'The changes in this PR have almost certainly already been merged to the target branch.', - ].join('\n') - - core.info(`PR #${item.number}: closed`) - - if (!dry) { - await github.rest.issues.createComment({ - ...context.repo, - issue_number: pull_number, - body, - }) - - await github.rest.pulls.update({ - ...context.repo, - pull_number, - state: 'closed', - }) - } - - return {} - } - } - // Check for any human reviews other than the PR author, GitHub actions and other GitHub apps. // Accounts could be deleted as well, so don't count them. const reviews = (