diff options
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/backport-pr.sh | 8 |
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." |
