From 4d6ec6958d29bd22739ba5fe27086e715d51fbc1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mike=20F=C3=A4hrmann?= <mike_faehrmann@web.de>
Date: Mon, 15 Jan 2024 22:37:33 +0100
Subject: [PATCH] [scripts] add 'push --force' to pull-request

---
 scripts/pull-request | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/scripts/pull-request b/scripts/pull-request
index defdc11f..dea9b292 100755
--- a/scripts/pull-request
+++ b/scripts/pull-request
@@ -41,6 +41,10 @@ case "${2,,}" in
     call git push "$USER" HEAD:"$BRANCH"
     ;;
 
+"pf"|"push-force")
+    call git push --force "$USER" HEAD:"$BRANCH"
+    ;;
+
 "d"|"delete")
     call git switch master
     call git branch -D "$USER-$BRANCH"