diff options
| author | zapashcanon | 2018-02-21 22:42:10 +0100 |
|---|---|---|
| committer | zapashcanon | 2018-04-05 22:05:43 +0100 |
| commit | 250502b01340ec6bedace85c6a2d4a4e57a107cf (patch) | |
| tree | 256fd7d0e38d2bdc24350eb18e61b0fb73e44215 /dev/tools/backport-pr.sh | |
| parent | b7938d0a51cdef8076bf5e1a58907b845a3fcc3d (diff) | |
Improve shell scripts
Diffstat (limited to 'dev/tools/backport-pr.sh')
| -rwxr-xr-x | dev/tools/backport-pr.sh | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index e4359f7038..5205350a61 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -27,9 +27,9 @@ BRANCH=backport-pr-${PRNUM} RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../') MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/') -if git checkout -b ${BRANCH}; then +if git checkout -b "${BRANCH}"; then - if ! git cherry-pick -x ${RANGE}; then + if ! git cherry-pick -x "${RANGE}"; then echo "Please fix the conflicts, then exit." bash while ! git cherry-pick --continue; do @@ -50,7 +50,7 @@ else fi -if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then +if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then echo read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r echo @@ -63,8 +63,8 @@ if [[ "${OPTION}" == "--stop-before-merging" ]]; then exit 0 fi -git merge -S --no-ff ${BRANCH} -m "${MESSAGE}" -git branch -d ${BRANCH} +git merge -S --no-ff "${BRANCH}" -m "${MESSAGE}" +git branch -d "${BRANCH}" # To-Do: # - Support for backporting a PR before it is merged |