aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/backport-pr.sh
diff options
context:
space:
mode:
authorJason Gross2020-05-24 13:02:52 -0400
committerJason Gross2020-05-24 13:02:52 -0400
commit16e0877c6e3ec6228875e10afb1ec17d640eb1e9 (patch)
treea0c89d53fd53bce124b585371f50689cf9ab44d2 /dev/tools/backport-pr.sh
parent2b8f1c3fb288c5647ddb427edba1c361eb5bc6b4 (diff)
parentdbefe0718913318b20d2c56e2ed026c638897a26 (diff)
Merge PR #12392: [backport-pr] Select correct remote of the master branch.
Reviewed-by: JasonGross
Diffstat (limited to 'dev/tools/backport-pr.sh')
-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..3fdc82b81b 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" || true)
+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."