blob: d18a583beec137a21abf90e16366ab2166c1e0e6 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
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" || 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
|
