From 0300aa85f3ba8cc7cdd38f719628dc0a28170c84 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 8 Jan 2018 23:56:30 +0100
Subject: Simplify logic and streamline lint-repository.sh

We inline should-check-whitespace.sh in check-eof-newline.sh
simplifying the find invocation.
---
 dev/tools/check-eof-newline.sh       | 19 ++++++++++++-------
 dev/tools/should-check-whitespace.sh |  6 ------
 2 files changed, 12 insertions(+), 13 deletions(-)
 delete mode 100755 dev/tools/should-check-whitespace.sh

(limited to 'dev/tools')

diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh
index 1c578c05ce..9e4c8661dc 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/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh
deleted file mode 100755
index d85d651070..0000000000
--- 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$'
-- 
cgit v1.2.3


From dfe41b6a564203c12a2fc2618f3082f971225022 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 9 Jan 2018 13:09:13 +0100
Subject: Cleanup shell expansions and quoting.

---
 dev/tools/merge-pr.sh | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'dev/tools')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 0c4a79bfd3..9c52644c63 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 "******************************************"
-- 
cgit v1.2.3


From 5d7e703f643930f2ba90767e75dee01d3e0c6fd6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 9 Jan 2018 16:49:19 +0100
Subject: merge-pr.sh: use git diff --quiet

---
 dev/tools/merge-pr.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/tools')

diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 9c52644c63..9f24960fff 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -43,7 +43,7 @@ fi;
 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 "******************************************"
-- 
cgit v1.2.3