From 59e7a45961a1ee1755df02512120c0b5bafe08ce Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 22 May 2020 22:41:47 +0200
Subject: [backport-pr] Select correct remote of the master branch.

---
 dev/tools/backport-pr.sh | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index 1ec8251f66..b1d2fd656a 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -30,7 +30,13 @@ while [[ $# -gt 0 ]]; do
     esac
 done
 
-MASTER=origin/master
+REMOTE=$(git config --get "branch.master.remote")
+if [ -z "$REMOTE" ]; then
+    echo "Branch master has no remote. Using the local state of the master branch instead."
+    MASTER=master
+else
+    MASTER="$REMOTE/master"
+fi
 
 if ! git log $MASTER --grep "Merge PR #$PRNUM" | grep "." > /dev/null; then
     echo "PR #${PRNUM} does not exist."
-- 
cgit v1.2.3