Skip to content

Commit 0b9e773

Browse files
authored
Merge pull request #5264 from dotty-staging/fix-5248
Fix #5248: Move generated doc to lampepfl/dotty-website
2 parents 6fcb8b8 + f8f982a commit 0b9e773

File tree

2 files changed

+14
-12
lines changed

2 files changed

+14
-12
lines changed

.drone.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ pipeline:
5252
image: lampepfl/dotty:2018-10-01
5353
commands:
5454
- ./project/scripts/genDocs
55-
secrets: [ bot_pass ]
55+
secrets: [ bot_token ]
5656
when:
5757
event: push
5858
# We only generate the documentation for the master branch

project/scripts/genDocs

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
#!/usr/bin/env bash
22

33
# Usage:
4-
# BOT_PASS=<dotty-bot password> ./genDocs
4+
# BOT_TOKEN=<dotty-bot password> ./genDocs
55

66
set -e
77

88
# set extended glob, needed for rm everything but x
99
shopt -s extglob
1010

11-
# make sure that BOT_PASS is set
12-
if [ -z "$BOT_PASS" ]; then
13-
echo "Error: BOT_PASS env unset, unable to push without password" 1>&2
11+
# make sure that BOT_TOKEN is set
12+
if [ -z "$BOT_TOKEN" ]; then
13+
echo "Error: BOT_TOKEN env unset, unable to push without password" 1>&2
1414
exit 1
1515
fi
1616

@@ -29,8 +29,14 @@ fi
2929
# save current head for commit message in gh-pages
3030
GIT_HEAD=$(git rev-parse HEAD)
3131

32+
33+
# set up remote and github credentials
34+
git remote add doc-remote "https://dotty-bot:$BOT_TOKEN@github.com/lampepfl/dotty-website.git"
35+
git config user.name "dotty-bot"
36+
git config user.email "[email protected]"
37+
3238
# check out correct branch
33-
git fetch origin gh-pages:gh-pages
39+
git fetch doc-remote gh-pages
3440
git checkout gh-pages
3541

3642
# move newly generated _site dir to $PWD
@@ -45,13 +51,9 @@ mv _site/* .
4551
# remove now empty _site dir
4652
rm -rf _site
4753

48-
# set github credentials
49-
git config user.name "dotty-bot"
50-
git config user.email "[email protected]"
51-
5254
# add all contents of $PWD to commit
5355
git add -A
5456
git commit -m "Update gh-pages site for $GIT_HEAD" || echo "nothing new to commit"
5557

56-
# push using dotty-bot to origin
57-
git push https://dotty-bot:$BOT_PASS@github.com/lampepfl/dotty.git || echo "couldn't push, since nothing was added"
58+
# push to doc-remote
59+
git push doc-remote || echo "couldn't push, since nothing was added"

0 commit comments

Comments
 (0)