diff options
| author | Jason Gross | 2020-05-24 13:02:52 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-24 13:02:52 -0400 |
| commit | 16e0877c6e3ec6228875e10afb1ec17d640eb1e9 (patch) | |
| tree | a0c89d53fd53bce124b585371f50689cf9ab44d2 /dev | |
| parent | 2b8f1c3fb288c5647ddb427edba1c361eb5bc6b4 (diff) | |
| parent | dbefe0718913318b20d2c56e2ed026c638897a26 (diff) | |
Merge PR #12392: [backport-pr] Select correct remote of the master branch.
Reviewed-by: JasonGross
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/tools/backport-pr.sh | 8 | ||||
| -rwxr-xr-x | dev/tools/generate-release-changelog.sh | 4 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 2 |
3 files changed, 10 insertions, 4 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." diff --git a/dev/tools/generate-release-changelog.sh b/dev/tools/generate-release-changelog.sh index 5b2d749b66..4533d39adc 100755 --- a/dev/tools/generate-release-changelog.sh +++ b/dev/tools/generate-release-changelog.sh @@ -31,14 +31,14 @@ if ! git diff --quiet; then ask_confirmation fi -remote=$(git config --get "branch.${branch}.remote") +remote=$(git config --get "branch.${branch}.remote" || true) if [ -z "$remote" ]; then echo "Warning: branch $branch has no associated remote." ask_confirmation else - if [ "$remote" != $(git config --get "branch.master.remote") ]; then + if [ "$remote" != $(git config --get "branch.master.remote" || true) ]; then echo "Warning: branch master and branch $branch do not have the same remote." ask_confirmation fi diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 82e4bd1e1e..7b450c3e53 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -99,7 +99,7 @@ info "PR $PR targets branch $BASE_BRANCH" CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) info "you are merging in $CURRENT_LOCAL_BRANCH" -REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote") +REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote" || true) if [ -z "$REMOTE" ]; then error "branch $CURRENT_LOCAL_BRANCH has not associated remote" error "don't know where to fetch the PR from" |