Commit d7948767 authored by Richard Levitte's avatar Richard Levitte
Browse files

Travis: if "make update" created a diff, please show it

parent de8c19cd
Loading
Loading
Loading
Loading
+1 −1
Original line number Diff line number Diff line
@@ -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';