diff options
| author | Felix Mulder <felix.mulder@gmail.com> | 2017-02-02 18:25:32 +0100 |
|---|---|---|
| committer | Felix Mulder <felix.mulder@gmail.com> | 2017-02-02 18:25:32 +0100 |
| commit | 8408ac9523bbb243556d1a9c8949ea2410003c72 (patch) | |
| tree | 763f7cd6407d8776eed2bd660d91115275874e36 /project | |
| parent | 480f248e95f5868431876f849b71605abfdfd114 (diff) | |
| download | dotty-8408ac9523bbb243556d1a9c8949ea2410003c72.tar.gz dotty-8408ac9523bbb243556d1a9c8949ea2410003c72.tar.bz2 dotty-8408ac9523bbb243556d1a9c8949ea2410003c72.zip | |
Change integrations to only fire on changed build status
Diffstat (limited to 'project')
| -rwxr-xr-x | project/scripts/genDocs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/project/scripts/genDocs b/project/scripts/genDocs index a657a06f3..d18a583be 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" || true + git commit -m "Update gh-pages site for $GIT_HEAD" || echo "nothing new to commit" # push using dotty-bot to origin - git push https://dotty-bot:$BOT_PASS@github.com/lampepfl/dotty.git || true + git push https://dotty-bot:$BOT_PASS@github.com/lampepfl/dotty.git || echo "couldn't push, since nothing was added" else # wrong parameter passed, should only generate docs if argument is "test" # to avoid multiple site gens |