re-instate the push-pr.sh script, since GHA won't have access to se…

…crets for PRs from external forks Co-authored-by: Andrew Nowak <[email protected]>
guardian · Oct 4, 2023 · 0e30f2a · 0e30f2a
1 parent 9ed8b92
commit 0e30f2a
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/dev/script/push-pr.sh b/dev/script/push-pr.sh
@@ -0,0 +1,16 @@
+#!/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}