[fix, CI] Push developer docs once again (#5243)

It's been broken since https://github.com/koreader/koreader/pull/3340 nearly two years ago.
pull/5245/head
Frans de Jonge 5 years ago committed by GitHub
parent da988c15de
commit a4e3e8b990
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

@ -37,7 +37,7 @@ EOF
echo -e "\\n${ANSI_GREEN}Pushing document update..."
git -c user.name="KOReader build bot" -c user.email="non-reply@koreader.rocks" \
commit -a --amend -m 'Automated documentation build from travis-ci.'
git push -f --quiet origin gh-pages >/dev/null
git push -f --quiet "https://${DOCS_GITHUB_TOKEN}@github.com/koreader/doc.git" gh-pages >/dev/null
echo -e "\\n${ANSI_GREEN}Documentation update pushed."
} && popd || exit

Loading…
Cancel
Save