File tree 2 files changed +5
-5
lines changed
2 files changed +5
-5
lines changed Original file line number Diff line number Diff line change @@ -710,7 +710,7 @@ jobs:
710
710
git config --global --add safe.directory /__w/scala3/scala3
711
711
./project/scripts/genDocs -doc-snapshot
712
712
713
- - name : Deploy Website to dotty-website
713
+ - name : Deploy Website to https:// dotty.epfl.ch
714
714
uses : peaceiris/actions-gh-pages@v4
715
715
with :
716
716
personal_token : ${{ secrets.DOTTYBOT_TOKEN }}
Original file line number Diff line number Diff line change @@ -5,7 +5,7 @@ shopt -s extglob # needed for rm everything but x
5
5
echo " Working directory: $PWD "
6
6
7
7
GENDOC_EXTRA_ARGS=$@
8
- GIT_HEAD=$( git rev-parse HEAD) # save current head for commit message in gh-pages
8
+ GIT_HEAD=$( git rev-parse HEAD) # save current head for commit message in scala/dotty.epfl.ch
9
9
PREVIOUS_SNAPSHOTS_DIR=" $PWD /../prev_snapshots"
10
10
SCRIPT_DIR=" $( cd " $( dirname " ${BASH_SOURCE[0]} " ) " >& /dev/null && pwd) "
11
11
SITE_OUT_DIR=" $PWD /docs/_site"
@@ -16,9 +16,9 @@ if [ -d "$PREVIOUS_SNAPSHOTS_DIR" ]; then
16
16
fi
17
17
18
18
mkdir -pv " $PREVIOUS_SNAPSHOTS_DIR "
19
- git remote add doc-remote " https://github.com/lampepfl /dotty-website .git"
20
- git fetch doc-remote gh-pages
21
- git checkout gh-pages
19
+ git remote add doc-remote " https://github.com/scala /dotty.epfl.ch .git"
20
+ git fetch doc-remote main
21
+ git checkout doc-remote/main
22
22
(cp -vr [03].* / " $PREVIOUS_SNAPSHOTS_DIR " ; true) # Don't fail if no `3.*` found to copy
23
23
git checkout " $GIT_HEAD "
24
24
You can’t perform that action at this time.
0 commit comments