aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-22 22:41:47 +0200
committerThéo Zimmermann2020-05-22 22:41:47 +0200
commit59e7a45961a1ee1755df02512120c0b5bafe08ce (patch)
tree2b8b6fb41d7fedb4c3d024b5e38592909f05e103 /dev/tools
parent127c61a5f2a448d33ef03c3093193dcfcee490fe (diff)
[backport-pr] Select correct remote of the master branch.
Diffstat (limited to 'dev/tools')
-rwxr-xr-xdev/tools/backport-pr.sh8
1 files changed, 7 insertions, 1 deletions
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."