Fix #5248: Move generated doc to lampepfl/dotty-website

Author: allanrenucci

.drone.yml

@@ -52,7 +52,7 @@ pipeline:
     image: lampepfl/dotty:2018-10-01
     commands:
       - ./project/scripts/genDocs
-    secrets: [ bot_pass ]
+    secrets: [ bot_token ]
     when:
       event: push
       # We only generate the documentation for the master branch

project/scripts/genDocs

@@ -1,19 +1,22 @@
 #!/usr/bin/env bash
 
 # Usage:
-# BOT_PASS=<dotty-bot password> ./genDocs
+# BOT_TOKEN=<dotty-bot password> ./genDocs
 
 set -e
 
 # set extended glob, needed for rm everything but x
 shopt -s extglob
 
-# make sure that BOT_PASS is set
-if [ -z "$BOT_PASS" ]; then
-    echo "Error: BOT_PASS env unset, unable to push without password" 1>&2
+# make sure that BOT_TOKEN is set
+if [ -z "$BOT_TOKEN" ]; then
+    echo "Error: BOT_TOKEN env unset, unable to push without password" 1>&2
     exit 1
 fi
 
+DOC_REMOTE="https://github.com/lampepfl/dotty-website.git"
+DOC_BRANCH="gh-pages"
+
 echo "Working directory: $PWD"
 
 # this command will generate docs in $PWD/docs/_site
@@ -30,8 +33,9 @@ fi
 GIT_HEAD=$(git rev-parse HEAD)
 
 # check out correct branch
-git fetch origin gh-pages:gh-pages
-git checkout gh-pages
+git remote add doc-remote "$DOC_REMOTE"
+git fetch doc-remote "$DOC_BRANCH"
+git checkout "$DOC_BRANCH"
 
 # move newly generated _site dir to $PWD
 mv $PWD/docs/_site .
@@ -47,11 +51,12 @@ rm -rf _site
 
 # set github credentials
 git config user.name "dotty-bot"
-git config user.email "[email protected]"
+git config user.email "[email protected]"
+git config user.password "$BOT_TOKEN"
 
 # 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"
+# push using dotty-bot to DOC_REMOTE
+git push doc-remote || echo "couldn't push, since nothing was added"