diff options
| author |  zapashcanon <leo@ndrs.fr> | 2018-02-21 22:42:10 +0100 |
|---|---|---|
| committer | zapashcanon <leo@ndrs.fr> | 2018-04-05 22:05:43 +0100 |
| commit | 250502b01340ec6bedace85c6a2d4a4e57a107cf (patch) | |
| tree | 256fd7d0e38d2bdc24350eb18e61b0fb73e44215 /dev/tools | |
| parent | b7938d0a51cdef8076bf5e1a58907b845a3fcc3d (diff) | |
Improve shell scripts
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/backport-pr.sh | 10 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 4 |
2 files changed, 7 insertions, 7 deletions
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index e4359f703..5205350a6 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 diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index ecfdfab94..20612eeb8 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -80,8 +80,8 @@ if [ -z "$REMOTE" ]; then exit 1 fi REMOTE_URL=$(git remote get-url "$REMOTE" --push) -if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" -a \ - "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then +if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" ] && \ + [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo" error "that is ${BLUE}$OFFICIAL_REMOTE_URL" error "it points to ${BLUE}$REMOTE_URL${RESET} instead" |