From bcb010db7d0d20f27e2693359002e4dc8736ce76 Mon Sep 17 00:00:00 2001 From: Felix Mulder Date: Thu, 2 Feb 2017 17:20:08 +0100 Subject: Fix slack integration and allow empty to gh-pages --- project/scripts/genDocs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'project') diff --git a/project/scripts/genDocs b/project/scripts/genDocs index b8d0ba254..a657a06f3 100755 --- a/project/scripts/genDocs +++ b/project/scripts/genDocs @@ -57,10 +57,10 @@ if [ "$1" = "test" ]; then # add all contents of $PWD to commit git add -A - git commit -m "Update gh-pages site for $GIT_HEAD" + git commit -m "Update gh-pages site for $GIT_HEAD" || true # push using dotty-bot to origin - git push https://dotty-bot:$BOT_PASS@github.com/lampepfl/dotty.git + git push https://dotty-bot:$BOT_PASS@github.com/lampepfl/dotty.git || true else # wrong parameter passed, should only generate docs if argument is "test" # to avoid multiple site gens -- cgit v1.2.3