diff options
| -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 "******************************************" |