1#!/bin/bash 2 3set -x 4set -o errexit -o nounset 5 6DOCSDIR=build-docs 7REVISION=$(git rev-parse --short HEAD) 8 9rm -rf $DOCSDIR || exit 10mkdir $DOCSDIR 11cd $DOCSDIR 12 13cp ../build/docs/html/* . 14#cp ../build/docs/CNAME . 15 16git init 17git branch -m main 18git config user.name "CI" 19git config user.email "harfbuzz-admin@googlegroups.com" 20set +x 21echo "git remote add upstream \"https://\$GH_TOKEN@github.com/harfbuzz/harfbuzz.github.io.git\"" 22git remote add upstream "https://$GH_TOKEN@github.com/harfbuzz/harfbuzz.github.io.git" 23set -x 24git fetch upstream 25git reset upstream/main 26 27touch . 28git add -A . 29 30if [[ $(git status -s) ]]; then 31 git commit -m "Rebuild docs for https://github.com/harfbuzz/harfbuzz/commit/$REVISION" 32 git push -q upstream HEAD:main 33fi 34