Merge branch 'main' into main

This commit is contained in:
is-a.dev Bot authored and GitHub committed 2026-08-19 13:51:37 +08:00
commit 487c979f24
1 file changed
+54
+54
View File
@@ -26,6 +26,8 @@ jobs:
with:
github-token: ${{ secrets.BOT }}
script: |
const marker = "<!-- is-a-dev-bot: merge-conflict -->";
const prs = await github.paginate(
github.rest.pulls.list,
{
@@ -49,5 +51,57 @@ jobs:
console.log(`Updated #${pr.number} (${pr.head.ref})`);
} catch (error) {
console.log(`Could not update #${pr.number}: ${error.message}`);
const { data: updatedPr } = await github.rest.pulls.get({
owner: context.repo.owner,
repo: context.repo.repo,
pull_number: pr.number
});
if (updatedPr.mergeable !== false) {
continue;
}
await github.rest.issues.addLabels({
owner: context.repo.owner,
repo: context.repo.repo,
issue_number: pr.number,
labels: ["reason: merge conflict"]
});
const comments = await github.paginate(
github.rest.issues.listComments,
{
owner: context.repo.owner,
repo: context.repo.repo,
issue_number: pr.number
}
);
const alreadyCommented = comments.some(
(comment) =>
comment.user?.login === "is-a-dev-bot" &&
comment.body?.includes(marker)
);
if (!alreadyCommented) {
const body = [
marker,
"## ❌ Merge conflict",
"",
"This pull request can not be merged because it has merge conflicts with `main`.",
"",
"***Please resolve the merge conflicts before this PR can be merged!***"
].join("\n");
await github.rest.issues.createComment({
owner: context.repo.owner,
repo: context.repo.repo,
issue_number: pr.number,
body
});
}
console.log(`Marked #${pr.number} as having merge conflicts`);
}
}