Skip to content
Find file
Fetching contributors…
Cannot retrieve contributors at this time
executable file 31 lines (27 sloc) 520 Bytes
#!/bin/bash
#
# Clone source repo, generate extension + web site, push to gh-pages
#
if [ $# -ne 2 ]; then
echo 'arguments: <main_repo_url> <tmp_dir>'
echo
exit
fi
MAIN_URL=$1
# DO NOT USE LOCAL TMP_DIR=./tmp ...
# otherwise 'git push' below will push to bot repo too
TMP_DIR=$2
#
# Pull main repo
#
rm -rf $TMP_DIR/web
cd $TMP_DIR
git clone $MAIN_URL web
#
# Generate extension + web page, then push
#
cd $TMP_DIR/web
make web
cd build/gh-pages
git commit -am 'Auto-updating via bot'
git push origin gh-pages
Something went wrong with that request. Please try again.