From f0b76e0bb5b61ad3f04313c6723363e4866e332f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mike=20F=C3=A4hrmann?= <mike_faehrmann@web.de>
Date: Thu, 4 May 2023 10:46:38 +0200
Subject: [PATCH] publish pull request helper script

it's what I've been using to manage GitHub pull requests locally
---
 scripts/pull-request | 55 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100755 scripts/pull-request

diff --git a/scripts/pull-request b/scripts/pull-request
new file mode 100755
index 00000000..defdc11f
--- /dev/null
+++ b/scripts/pull-request
@@ -0,0 +1,55 @@
+#!/bin/bash
+set -e
+
+RE="https://github.com/([^/?#]+)/([^/?#]+)(/tree/(.+))?"
+if [[ "$1" =~ $RE ]]; then
+    USER="${BASH_REMATCH[1]}"
+    REPO="${BASH_REMATCH[2]}"
+    BRANCH="${BASH_REMATCH[4]:-master}"
+
+else
+    echo "invalid github repository identifier: '$1'"
+    exit 1
+
+fi
+
+
+call() { echo "$@"; "$@"; echo; }
+
+# {x,,} transforms value to lowercase
+case "${2,,}" in
+
+""|"f"|"fetch")
+    call git remote add "$USER" git@github.com:"$USER"/"$REPO".git || true
+    call git fetch "$USER" "$BRANCH"
+    call git checkout -b "$USER-$BRANCH" "$USER/$BRANCH"
+    ;;
+
+"m"|"merge")
+    RE='\s*(.+)\s+#([0-9]+)'
+    if [[ "$3" =~ $RE ]]; then
+        TITLE="${BASH_REMATCH[1]}"
+        PULL="${BASH_REMATCH[2]}"
+    fi
+
+    call git switch master
+    call git merge --no-ff --edit -m "merge #${PULL-_}: ${TITLE-_}" "$USER-$BRANCH"
+    call git branch -d "$USER-$BRANCH"
+    ;;
+
+"p"|"push")
+    call git push "$USER" HEAD:"$BRANCH"
+    ;;
+
+"d"|"delete")
+    call git switch master
+    call git branch -D "$USER-$BRANCH"
+    call git remote remove "$USER"
+    ;;
+
+*)
+    echo "invalid action: '$2'"
+    exit 2
+    ;;
+
+esac