Update push.sh

This commit is contained in:
David Wu
2017-12-25 19:02:13 +01:00
committed by GitHub
parent 23562d1cf0
commit 7ad3c2f5ed

View File

@ -6,7 +6,7 @@ setup_git() {
commit_website_files() {
git checkout master
if [[ $(( $TRAVIS_BUILD_NUMBER % 5 )) == 0 ]]; then
n = $(( ($TRAVIS_BUILD_NUMBER-270)/5))
declare -i n=($TRAVIS_BUILD_NUMBER-270)/5
npm run linter
echo "Linting build: $n"
fi