Fail if `git diff` fails
Change-Id: I57256b0a24247f6123cb0e25a89c1b59867cb3f9
This commit is contained in:
parent
4c39ed9d7f
commit
9cb2c56dc1
|
@ -50,6 +50,7 @@ matrix:
|
|||
- binutils-mingw-w64-i686 gcc-mingw-w64-i686 g++-mingw-w64-i686
|
||||
|
||||
script:
|
||||
- set -o pipefail
|
||||
- git diff `git merge-base master HEAD` | ./tools/scripts/checkpatch.pl -
|
||||
- ./bootstrap && ./configure --enable-remote-bitbang --enable-jtag_vpi $CONFIGURE_ARGS && make
|
||||
- file src/$EXECUTABLE
|
||||
|
|
Loading…
Reference in New Issue