1#!/bin/bash 2 3set -o errexit -o nounset 4 5rev=$(git rev-parse --short HEAD) 6 7cd target/doc 8 9git init 10git config user.email 'FlashCat@users.noreply.github.com' 11git config user.name 'FlashCat' 12git remote add upstream "https://${GH_TOKEN}@github.com/${TRAVIS_REPO_SLUG}.git" 13git fetch upstream gh-pages 14git reset upstream/gh-pages 15 16touch . 17 18git add -A . 19git commit -m "rebuild pages at ${rev}" 20git push -q upstream HEAD:gh-pages 21