blob: 73e034276a8f82e3a3a6862a140ad5569d25b16d (
plain) (
tree)
|
|
#!/usr/bin/env bash
# Usage: ./genDocs <test variable> <dotty-bot password>
set -e
# set extended glob, needed for rm everything but x
shopt -s extglob
if [ "$1" = ";dotty-compiler/testOnly dotty.tools.dotc.CompilationTests" ]; then
# make sure that BOT_PASS is set
if [ -z ${2+x} ]; then
echo "BOT_PASS unset, unable to push without password" 1>&2
exit 1
else
BOT_PASS=$2
fi
echo "Working directory: $PWD"
# this command will generate docs in $PWD/docs/_site
sbt -J-Xmx4096m \
-J-XX:ReservedCodeCacheSize=512m \
-J-XX:MaxMetaspaceSize=1024m \
-Ddotty.drone.mem=4096m \
-ivy /var/cache/drone/ivy2 \
"genDocs"
# make sure that the previous command actually succeeded
if [ ! -d "$PWD/docs/_site" ]; then
echo "Output directory did not exist: $PWD/docs/_site" 1>&2
exit 1
fi
# save current head for commit message in gh-pages
GIT_HEAD=$(git rev-parse HEAD)
# check out correct branch
git fetch origin gh-pages:gh-pages
git checkout gh-pages
# move newly generated _site dir to $PWD
mv $PWD/docs/_site .
# remove everything BUT _site dir
rm -rf !(_site)
# copy new contents to $PWD
mv _site/* .
# remove now empty _site dir
rm -rf _site
# set github credentials
git config user.name "dotty-bot"
git config user.email "felix.mulder@epfl.ch"
# add all contents of $PWD to commit
git add -A
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 || 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
echo "Not generating docs for $1"
fi
|