mirror of
https://github.com/RIOT-OS/RIOT.git
synced 2025-01-17 05:12:57 +01:00
dist/whitespacecheck: use result of piped command for return value
This commit is contained in:
parent
e5f5f3c0b3
commit
6208515a86
6
dist/tools/whitespacecheck/check.sh
vendored
6
dist/tools/whitespacecheck/check.sh
vendored
@ -1,4 +1,4 @@
|
||||
#!/bin/sh
|
||||
#!/bin/bash
|
||||
|
||||
# Copyright 2015 Oliver Hahm <oliver.hahm@inria.fr>
|
||||
#
|
||||
@ -38,7 +38,7 @@ fi
|
||||
git -c core.whitespace="tab-in-indent,tabwidth=4" \
|
||||
diff --check "$(git merge-base "${BRANCH}" HEAD)" -- *.[ch] ${IGNORE} \
|
||||
| ${LOG}
|
||||
RESULT=$?
|
||||
RESULT=${PIPESTATUS[0]}
|
||||
|
||||
# Git regards any trailing white space except `\n` as an error so `\r` is
|
||||
# checked here, too
|
||||
@ -46,7 +46,7 @@ git -c core.whitespace="trailing-space" \
|
||||
diff --check "$(git merge-base "${BRANCH}" HEAD)" -- . ${IGNORE} \
|
||||
| ${LOG}
|
||||
|
||||
TRAILING_RESULT=$?
|
||||
TRAILING_RESULT=${PIPESTATUS[0]}
|
||||
|
||||
github_annotate_parse_log_default
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user