diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-23 09:54:31 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-23 09:54:31 +0100 |
commit | 969926a5b042d1850b262fb62dbd1d0d8534babe (patch) | |
tree | 4296fea1c2bef09ed9a0605a8328672181872c18 /dev/tools | |
parent | 35a275e22b72abba344b837e7276af8057d5da2c (diff) | |
parent | 5d7e703f643930f2ba90767e75dee01d3e0c6fd6 (diff) |
Merge PR #6568: Cleanup scripts
Diffstat (limited to 'dev/tools')
-rwxr-xr-x | dev/tools/check-eof-newline.sh | 19 | ||||
-rwxr-xr-x | dev/tools/merge-pr.sh | 20 | ||||
-rwxr-xr-x | dev/tools/should-check-whitespace.sh | 6 |
3 files changed, 22 insertions, 23 deletions
diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh index 1c578c05c..9e4c8661d 100755 --- a/dev/tools/check-eof-newline.sh +++ b/dev/tools/check-eof-newline.sh @@ -1,9 +1,14 @@ #!/usr/bin/env bash -if [ -z "$(tail -c 1 "$1")" ] -then - exit 0 -else - echo "No newline at end of file $1!" - exit 1 -fi +CODE=0 +for f in "$@"; do + if git ls-files --error-unmatch "$f" >/dev/null 2>&1 && \ + git check-attr whitespace -- "$f" | grep -q -v -e 'unset$' -e 'unspecified$' && \ + [ -n "$(tail -c 1 "$f")" ] + then + echo "No newline at end of file $f!" + CODE=1 + fi +done + +exit "$CODE" diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 0c4a79bfd..9f24960ff 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 --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then echo "******************************************" echo "** WARNING: does this PR have overlays? **" echo "******************************************" diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh deleted file mode 100755 index d85d65107..000000000 --- a/dev/tools/should-check-whitespace.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/usr/bin/env bash - -# determine if a file has whitespace checking enabled in .gitattributes - -git ls-files --error-unmatch "$1" >/dev/null 2>&1 && -git check-attr whitespace -- "$1" | grep -q -v -e 'unset$' -e 'unspecified$' |