From 43f3fcc5550741d433fa720c5d7673f1c8fe8b44 Mon Sep 17 00:00:00 2001
From: Wolfgang Walther <walther@technowledgy.de>
Date: Mon, 3 Nov 2025 12:08:21 +0100
Subject: [PATCH] ci/github-script/merge: fix with deleted users

When a deleted user had approved a PR, this will cause the merge-bot to
fail.
---
 ci/github-script/merge.js | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/ci/github-script/merge.js b/ci/github-script/merge.js
index c738ecc950f5..d7ed249ce4c3 100644
--- a/ci/github-script/merge.js
+++ b/ci/github-script/merge.js
@@ -34,7 +34,9 @@ function runChecklist({
           // bad code between the approval and the merge.
           commit_id === pull_request.head.sha,
       )
-      .map(({ user }) => user.id),
+      .map(({ user }) => user?.id)
+      // Some users have been deleted, so filter these out.
+      .filter(Boolean),
   )
 
   const checklist = {
@@ -158,12 +160,14 @@ async function handleMerge({
   )
 
   const comments = events.slice(lastPush + 1).filter(
-    ({ event, body, node_id }) =>
+    ({ event, body, user, node_id }) =>
       ['commented', 'reviewed'].includes(event) &&
       hasMergeCommand(body) &&
+      // Ignore comments where the user has been deleted already.
+      user &&
       // Ignore comments which had already been responded to by the bot.
       !events.some(
-        ({ event, user, body }) =>
+        ({ event, body }) =>
           ['commented'].includes(event) &&
           // We're only testing this hidden reference, but not the author of the comment.
           // We'll just assume that nobody creates comments with this marker on purpose.