Travis: if "make update" created a diff, please show it
@@ -168,7 +168,7 @@ script:
else
echo -e '+\057 MAKE UPDATE FAILED'; false;
fi;
- git diff --quiet
+ git diff --exit-code
- if [ -n "$CHECKDOCS" ]; then
if $make doc-nits; then
echo -e '+\057\057 MAKE DOC-NITS OK';
