Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- diff --git a/github-merge-pr.sh b/github-merge-pr.sh
- index f7325db..37022a9 100755
- --- a/github-merge-pr.sh
- +++ b/github-merge-pr.sh
- @@ -59,11 +59,6 @@ if [ "$(echo "$PR_INFO" | jq -r ".maintainer_can_modify")" == "false" ]; then
- exit 4
- fi
- -if [ "$(echo "$PR_INFO" | jq -r ".mergeable")" == "false" ]; then
- - echo "PR #$PRID is not mergeable for Github.com. Check the PR!" >&2
- - exit 5
- -fi
- -
- echo "Pulling current $BRANCH from origin"
- $GIT checkout $BRANCH
- $GIT fetch origin
- @@ -76,7 +71,7 @@ fi
- PR_USER="$(echo "$PR_INFO" | jq -r ".head.user.login")"
- PR_BRANCH="$(echo "$PR_INFO" | jq -r ".head.ref")"
- LOCAL_PR_BRANCH="$PR_BRANCH"-"$PR_USER"
- -PR_REPO="$(echo "$PR_INFO" | jq -r ".head.repo.html_url")"
- +PR_REPO="$(echo "$PR_INFO" | jq -r ".head.repo.ssh_url")"
- if ! $GIT remote get-url $PR_USER &> /dev/null || [ -n "$DRY_RUN" ]; then
- echo "Adding $PR_USER with repo $PR_REPO to remote"
- @@ -98,6 +93,8 @@ if ! $GIT rebase origin/$BRANCH; then
- exit 9
- fi
- +GIT="echo git"
- +
- echo "Force pushing $LOCAL_PR_BRANCH to HEAD:$PR_BRANCH for $PR_USER"
- if ! $GIT push $PR_USER HEAD:$PR_BRANCH --force; then
- echo "Failed to force push HEAD to $PR_USER" >&2
- @@ -107,11 +104,6 @@ fi
- echo "Returning to $BRANCH"
- $GIT checkout $BRANCH
- -if [ -n "$($GIT log origin/$BRANCH..HEAD)" ]; then
- - echo "Working on dirty branch for $BRANCH! Please reset $BRANCH to origin/$BRANCH" >&2
- - exit 10
- -fi
- -
- echo "Actually merging the PR #$PRID from branch $PR_USER/$PR_BRANCH"
- if ! $GIT merge --ff-only $PR_USER/$PR_BRANCH; then
- echo "Failed to merge $PR_USER/$PR_BRANCH on $BRANCH" >&2
Advertisement
Add Comment
Please, Sign In to add comment