From 497768c5205178f3e57cf7500432738316760077 Mon Sep 17 00:00:00 2001 From: Hamza Remmal Date: Wed, 18 Sep 2024 09:17:36 +0200 Subject: [PATCH] Adapt scripts to scala/dotty.epfl.ch not lampepfl/dotty-website --- .github/workflows/ci.yaml | 2 +- project/scripts/genDocs | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 309820f8f138..196952247892 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -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 }} diff --git a/project/scripts/genDocs b/project/scripts/genDocs index aa061d59b613..9849dac91722 100755 --- a/project/scripts/genDocs +++ b/project/scripts/genDocs @@ -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" @@ -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"