Maybe fix `deploy.sh`

diff --git a/.github/deploy.sh b/.github/deploy.sh
index 15b14e64a78dcd1356b81f39cb753d3facd9dfc3..98b61ca7b52d527df3d571ea973d325eec09ff74 100755 (executable)
--- a/.github/deploy.sh
+++ b/.github/deploy.sh
@@ -44,7 +44,8 @@ cd out
 git config user.name "Travis CI"
 git config user.email "travis@ci.invalid"
 
-if [ -z "$(git diff --exit-code)" ]; then
+git diff --exit-code
+if [ $? != 1 ]; then
     echo "No changes to the output on this push; exiting."
     exit 0
 fi