From 5d7e703f643930f2ba90767e75dee01d3e0c6fd6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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 9c52644c6..9f24960ff 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