max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0 path in script/pre-push

Browse source
This commit is contained in:
Sebastian Ullrich 2019-11-15 18:29:57 +01:00
parent b8d5193ecc
commit aa380ff505
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
script/pre-push
View file

@ -4,12 +4,12 @@ DIR="$( cd "$( dirname "$0" )" && pwd )"
CHECKER=$DIR/../../src/cmake/Modules/cpplint.py
while read local_ref local_sha remote_ref remote_sha;
do
CHANGED_FILES=`git diff --name-only $local_sha $remote_sha | grep '\(cpp\|h\)$' | grep -v 'src/stage0/'`
CHANGED_FILES=`git diff --name-only $local_sha $remote_sha | grep '\(cpp\|h\)$' | grep -v 'stage0/'`
if [ ! -z "$CHANGED_FILES" -a "$CHANGED_FILES" != " " ]; then
echo $CHANGED_FILES | xargs $CHECKER
RET=$?
if [ $RET -ne 0 ]; then
echo "There is error(s) from style-check. Please fix them before push to the repo."
echo "There are error(s) from style-check. Please fix them before pushing to the repo."
exit $RET
fi
fi