diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-09 13:09:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-16 16:27:07 +0100 |
| commit | dfe41b6a564203c12a2fc2618f3082f971225022 (patch) | |
| tree | 7f7576d0032a16acaa21fa6cb3af755349e2c9ab /dev/tools | |
| parent | 0300aa85f3ba8cc7cdd38f719628dc0a28170c84 (diff) | |
Cleanup shell expansions and quoting.
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/merge-pr.sh | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 0c4a79bfd..9c52644c6 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -9,18 +9,18 @@ set -e PR=$1 -CURRENT_LOCAL_BRANCH=`git rev-parse --abbrev-ref HEAD` -REMOTE=`git config --get branch.$CURRENT_LOCAL_BRANCH.remote` -git fetch $REMOTE refs/pull/$PR/head +CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) +REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote") +git fetch "$REMOTE" "refs/pull/$PR/head" API=https://api.github.com/repos/coq/coq -BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'` +BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label') -COMMIT=`git rev-parse FETCH_HEAD` -STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'` +COMMIT=$(git rev-parse FETCH_HEAD) +STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state') -if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then +if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then echo "Wrong base branch" read -p "Bypass? [y/N] " -n 1 -r echo @@ -30,7 +30,7 @@ if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then fi fi; -if [ $STATUS != "success" ]; then +if [ "$STATUS" != "success" ]; then echo "CI status is \"$STATUS\"" read -p "Bypass? [y/N] " -n 1 -r echo @@ -40,10 +40,10 @@ if [ $STATUS != "success" ]; then fi fi; -git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e +git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e # TODO: improve this check -if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then +if [[ $(git diff "$REMOTE/$CURRENT_LOCAL_BRANCH" dev/ci) ]]; then echo "******************************************" echo "** WARNING: does this PR have overlays? **" echo "******************************************" |