diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-09 16:49:19 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-16 16:27:07 +0100 |
| commit | 5d7e703f643930f2ba90767e75dee01d3e0c6fd6 (patch) | |
| tree | 9af7cc10602784b049a259c242f2cd06ce1ba6f5 /dev/tools | |
| parent | 0be785a5832177efa4ec396a421a4eb367b81914 (diff) | |
merge-pr.sh: use git diff --quiet
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/merge-pr.sh | 2 |
1 files changed, 1 insertions, 1 deletions
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 "******************************************" |