Loading ci/github-script/bot.js +0 −43 Original line number Diff line number Diff line Loading @@ -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 = ( Loading Loading
ci/github-script/bot.js +0 −43 Original line number Diff line number Diff line Loading @@ -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 = ( Loading