Skip to content

Commit

Permalink
Adapt scripts to scala/dotty.epfl.ch not lampepfl/dotty-website
Browse files Browse the repository at this point in the history
  • Loading branch information
hamzaremmal committed Sep 18, 2024
1 parent 6e852d2 commit 497768c
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 5 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/ci.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -710,7 +710,7 @@ jobs:
git config --global --add safe.directory /__w/scala3/scala3
./project/scripts/genDocs -doc-snapshot
- name: Deploy Website to dotty-website
- name: Deploy Website to https://dotty.epfl.ch
uses: peaceiris/actions-gh-pages@v4
with:
personal_token: ${{ secrets.DOTTYBOT_TOKEN }}
Expand Down
8 changes: 4 additions & 4 deletions project/scripts/genDocs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ shopt -s extglob # needed for rm everything but x
echo "Working directory: $PWD"

GENDOC_EXTRA_ARGS=$@
GIT_HEAD=$(git rev-parse HEAD) # save current head for commit message in gh-pages
GIT_HEAD=$(git rev-parse HEAD) # save current head for commit message in scala/dotty.epfl.ch
PREVIOUS_SNAPSHOTS_DIR="$PWD/../prev_snapshots"
SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" >& /dev/null && pwd)"
SITE_OUT_DIR="$PWD/docs/_site"
Expand All @@ -16,9 +16,9 @@ if [ -d "$PREVIOUS_SNAPSHOTS_DIR" ]; then
fi

mkdir -pv "$PREVIOUS_SNAPSHOTS_DIR"
git remote add doc-remote "https://github.com/lampepfl/dotty-website.git"
git fetch doc-remote gh-pages
git checkout gh-pages
git remote add doc-remote "https://github.com/scala/dotty.epfl.ch.git"
git fetch doc-remote main
git checkout doc-remote/main
(cp -vr [03].*/ "$PREVIOUS_SNAPSHOTS_DIR"; true) # Don't fail if no `3.*` found to copy
git checkout "$GIT_HEAD"

Expand Down

0 comments on commit 497768c

Please sign in to comment.