diff options
Diffstat (limited to 'project/scripts')
-rwxr-xr-x | project/scripts/genDocs | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/project/scripts/genDocs b/project/scripts/genDocs new file mode 100755 index 000000000..b8d0ba254 --- /dev/null +++ b/project/scripts/genDocs @@ -0,0 +1,68 @@ +#!/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" = "test" ]; 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" + + # push using dotty-bot to origin + git push https://dotty-bot:$BOT_PASS@github.com/lampepfl/dotty.git +else + # wrong parameter passed, should only generate docs if argument is "test" + # to avoid multiple site gens + echo "Not generating docs for $1" +fi |