|
| 1 | +#!/bin/bash -eux |
| 2 | + |
| 3 | +# |
| 4 | +# This variable must be passed into this script. |
| 5 | +# |
| 6 | +[[ -n "${BRANCH}" ]] || exit 1 |
| 7 | + |
| 8 | +# |
| 9 | +# We need these config parameters set in order to do the git-merge. |
| 10 | +# |
| 11 | +git config user.name "${GITHUB_ACTOR}" |
| 12 | +git config user.email "${GITHUB_ACTOR}@users.noreply.github.com" |
| 13 | + |
| 14 | +# |
| 15 | +# We need the full git repository history in order to do the git-merge. |
| 16 | +# |
| 17 | +git fetch --unshallow |
| 18 | + |
| 19 | +# |
| 20 | +# In order to open a pull request, we need to push to a remote branch. |
| 21 | +# To avoid conflicting with existing remote branches, we use branches |
| 22 | +# within the "sync-with-master" namespace. |
| 23 | +# |
| 24 | +git checkout -b "sync-with-master/${BRANCH}" "origin/${BRANCH}" |
| 25 | +git merge -Xtheirs origin/master |
| 26 | +git push -f origin "sync-with-master/${BRANCH}" |
| 27 | + |
| 28 | +# |
| 29 | +# Opening a pull request may fail if there already exists a pull request |
| 30 | +# for the branch; e.g. if a previous pull request was previously made, |
| 31 | +# but not yet merged by the time we run this "sync" script again. Thus, |
| 32 | +# rather than causing the automation to report a failure in this case, |
| 33 | +# we swallow the error and report success. |
| 34 | +# |
| 35 | +# Additionally, as along as the git branch was properly updated (via the |
| 36 | +# "git push" above), the existing PR will have been updated as well, so |
| 37 | +# the "hub" command is unnecessary (hence ignoring the error). |
| 38 | +# |
| 39 | +git log -1 --format=%B | hub pull-request -F - -b "${BRANCH}" || true |
0 commit comments