From 7c0c1441b37dc7e04d8e0b0097b3d9f92a5d6b67 Mon Sep 17 00:00:00 2001
From: Tom Richards <tom.richards@guardian.co.uk>
Date: Mon, 22 Jan 2024 15:06:31 +0000
Subject: [PATCH] replace `dev/script/push-pr.sh` with an equivalent GHA via
 `workflow_dispatch` i.e. manual invocation for better developer experience

---
 .github/workflows/push-pr.yml | 26 ++++++++++++++++++++++++++
 dev/script/push-pr.sh         | 16 ----------------
 2 files changed, 26 insertions(+), 16 deletions(-)
 create mode 100644 .github/workflows/push-pr.yml
 delete mode 100755 dev/script/push-pr.sh

diff --git a/.github/workflows/push-pr.yml b/.github/workflows/push-pr.yml
new file mode 100644
index 0000000000..5a293fb19b
--- /dev/null
+++ b/.github/workflows/push-pr.yml
@@ -0,0 +1,26 @@
+name: push-pr
+on:
+  workflow_dispatch:
+    inputs:
+      prNumber:
+        description: 'PR number'
+        required: true
+        type: string
+  # we decided not to have 'workflow_run' here (chained off CI success) for 'trusted' forks, as we don't know/control the
+  # access control etc. - so keeping it manual only (via workflow_dispatch above)
+  # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run:
+
+jobs:
+  push-pr:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+    steps:
+      - uses: actions/checkout@v4
+      - name: push-pr
+        env:
+          PR: ${{ inputs.prNumber }}
+        run: |
+          echo "Pushing PR merge commit for ${PR} to remote pr${PR} branch"
+          git fetch -f origin pull/${PR}/merge:pr${PR}
+          git push -f origin pr${PR}:pr${PR}
diff --git a/dev/script/push-pr.sh b/dev/script/push-pr.sh
deleted file mode 100755
index c3a7273bf8..0000000000
--- a/dev/script/push-pr.sh
+++ /dev/null
@@ -1,16 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-
-
-if [ -z $1 ]
-then
-  echo "Please run this script with a PR number as its argument."
-  exit 1
-fi
-
-PR=$1
-
-echo "Pushing PR merge commit for ${PR} to remote pr${PR} branch"
-git fetch -f origin pull/${PR}/merge:pr${PR}
-git push -f origin pr${PR}:pr${PR}