Guest User

Untitled

a guest
May 16th, 2023
61
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 1.59 KB | None | 0 0
  1. diff --git a/github-merge-pr.sh b/github-merge-pr.sh
  2. index f7325db..37022a9 100755
  3. --- a/github-merge-pr.sh
  4. +++ b/github-merge-pr.sh
  5. @@ -59,11 +59,6 @@ if [ "$(echo "$PR_INFO" | jq -r ".maintainer_can_modify")" == "false" ]; then
  6. exit 4
  7. fi
  8.  
  9. -if [ "$(echo "$PR_INFO" | jq -r ".mergeable")" == "false" ]; then
  10. - echo "PR #$PRID is not mergeable for Github.com. Check the PR!" >&2
  11. - exit 5
  12. -fi
  13. -
  14. echo "Pulling current $BRANCH from origin"
  15. $GIT checkout $BRANCH
  16. $GIT fetch origin
  17. @@ -76,7 +71,7 @@ fi
  18. PR_USER="$(echo "$PR_INFO" | jq -r ".head.user.login")"
  19. PR_BRANCH="$(echo "$PR_INFO" | jq -r ".head.ref")"
  20. LOCAL_PR_BRANCH="$PR_BRANCH"-"$PR_USER"
  21. -PR_REPO="$(echo "$PR_INFO" | jq -r ".head.repo.html_url")"
  22. +PR_REPO="$(echo "$PR_INFO" | jq -r ".head.repo.ssh_url")"
  23.  
  24. if ! $GIT remote get-url $PR_USER &> /dev/null || [ -n "$DRY_RUN" ]; then
  25. echo "Adding $PR_USER with repo $PR_REPO to remote"
  26. @@ -98,6 +93,8 @@ if ! $GIT rebase origin/$BRANCH; then
  27. exit 9
  28. fi
  29.  
  30. +GIT="echo git"
  31. +
  32. echo "Force pushing $LOCAL_PR_BRANCH to HEAD:$PR_BRANCH for $PR_USER"
  33. if ! $GIT push $PR_USER HEAD:$PR_BRANCH --force; then
  34. echo "Failed to force push HEAD to $PR_USER" >&2
  35. @@ -107,11 +104,6 @@ fi
  36. echo "Returning to $BRANCH"
  37. $GIT checkout $BRANCH
  38.  
  39. -if [ -n "$($GIT log origin/$BRANCH..HEAD)" ]; then
  40. - echo "Working on dirty branch for $BRANCH! Please reset $BRANCH to origin/$BRANCH" >&2
  41. - exit 10
  42. -fi
  43. -
  44. echo "Actually merging the PR #$PRID from branch $PR_USER/$PR_BRANCH"
  45. if ! $GIT merge --ff-only $PR_USER/$PR_BRANCH; then
  46. echo "Failed to merge $PR_USER/$PR_BRANCH on $BRANCH" >&2
Advertisement
Add Comment
Please, Sign In to add comment