Skip to content

Adds scripts to fetch/push PR branches #70

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
braughtg wants to merge 1 commit into
base: development
Choose a base branch
from
Open

Adds scripts to fetch/push PR branches #70

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
49 changes: 49 additions & 0 deletions bin/fetchPR.bash
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
#!/bin/bash
# Fetch a PR from the upstream repository
# The branch for the PR is fetched from the author's fork.
# Assuming the PR author granted managers write access to the
# branch, this will allow the fetched branch to be edited and pushed
# back using pushPR.bash.

source colors.bash
source lib.bash

function usage {
echo "fetchPR.bash usage:"
echo " fetchPR.bash <PR Number>"
exit 1
}

if [ $# -ne 1 ]; then
usage
fi

echo "Fetching PR $1..."
echo " Getting PR information..."
PR_DATA=$(gh pr view "$1" --json headRefName --json headRepository --json headRepositoryOwner)
error_check "Unable to get PR data from GitHub."
PR_OWNER=$(echo "$PR_DATA" | jq -r '.headRepositoryOwner.login')
PR_REPO=$(echo "$PR_DATA" | jq -r '.headRepository.name')
PR_BRANCH=$(echo "$PR_DATA" | jq -r '.headRefName')
PR_LOCATION="$PR_OWNER/$PR_REPO/$PR_BRANCH"
echo " Found PR $1 at $PR_LOCATION"

BRANCH_EXISTS=$(git branch -a | grep "pr-$1-$PR_BRANCH")
if [[ "$BRANCH_EXISTS" == *"pr-$1-$PR_BRANCH"* ]]; then
echo -e "${ON_RED}ERROR:${NO_COLOR} The branch pr-$1-$PR_BRANCH already exists."
echo "Delete that branch."
echo "Then run this script again."
exit 1
fi

echo " Fetching $PR_LOCATION as PR-$1-$PR_BRANCH..."
git fetch --quiet "https://github.com/$PR_OWNER/$PR_REPO" "$PR_BRANCH:pr-$1-$PR_BRANCH"
error_check "Unable to fetch $PR_LOCATION as pr-$1-$PR_BRANCH."
echo " Fetched."

echo " Switching to branch pr-$1-$PR_BRANCH..."
git switch --quiet "pr-$1-$PR_BRANCH"
error_check "Unable to switch to branch pr-$1-$PR_BRANCH."
echo " Switched."

echo "Done."
44 changes: 44 additions & 0 deletions bin/pushPR.bash
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
#!/bin/bash
# Push the a PR branch fetched with fetchPR.bash back
# to the PR author's fork to update the PR with local
# edits.

source colors.bash
source lib.bash

function usage {
echo "pushPR.bash usage:"
echo " pushPR.bash <PR Number>"
exit 1
}

if [ $# -ne 1 ]; then
usage
fi

echo "Pushing PR $1..."
echo " Getting PR information..."
PR_DATA=$(gh pr view "$1" --json headRefName --json headRepository --json headRepositoryOwner)
error_check "Unable to get PR data from GitHub."
PR_OWNER=$(echo "$PR_DATA" | jq -r '.headRepositoryOwner.login')
PR_REPO=$(echo "$PR_DATA" | jq -r '.headRepository.name')
PR_BRANCH=$(echo "$PR_DATA" | jq -r '.headRefName')
PR_LOCATION="$PR_OWNER/$PR_REPO/$PR_BRANCH"
echo " Found PR $1 at $PR_LOCATION"

# Check that we are on the branch for the PR created by fetchPR.bash
CUR_BRANCH=$(git branch --show-current)
error_check "Unable to determine current branch."
if [ "$CUR_BRANCH" != "pr-$1-$PR_BRANCH" ]; then
echo -e "${ON_RED}ERROR:${NO_COLOR} Must be on the PR branch to push a PR."
echo "Switch to the pr-$1-$PR_BRANCH branch."
echo "Then run this script again."
exit 1
fi

echo " Pushing $PR_LOCATION..."
git push --quiet "https://github.com/$PR_OWNER/$PR_REPO" "pr-$1-$PR_BRANCH:$PR_BRANCH"
error_check "Unable to push $PR_LOCATION."
echo " Pushed."

echo "Done."