diff --git a/.travisci/pub_html.sh b/.travisci/pub_html.sh index 2c75c4083..14b176af4 100755 --- a/.travisci/pub_html.sh +++ b/.travisci/pub_html.sh @@ -30,6 +30,11 @@ else exit 0 fi +if [ `git rev-list HEAD...origin/$TRAVIS_BRANCH --count` != 0 ]; then + echo "We are outdated. Won't publish." + exit 0 +fi + git config --global user.name "${BOT_NAME}" git config --global user.email "${BOT_EMAIL}" git config --global push.default simple diff --git a/.travisci/pub_org.sh b/.travisci/pub_org.sh index fba6e9615..c22732bcc 100755 --- a/.travisci/pub_org.sh +++ b/.travisci/pub_org.sh @@ -28,6 +28,11 @@ else exit 0 fi +if [ `git rev-list HEAD...origin/$TRAVIS_BRANCH --count` != 0 ]; then + echo "We are outdated. Won't publish." + exit 0 +fi + git config --global user.name "${BOT_NAME}" git config --global user.email "${BOT_EMAIL}" git config --global push.default simple