From 0856d7b7c1f758d496f6c33d78d1c6e8fbe261c3 Mon Sep 17 00:00:00 2001 From: vincenzobaz Date: Wed, 9 Jun 2021 10:35:31 +0200 Subject: [PATCH 1/2] Copy old site versions for Scala 3 instead of Dotty 0.X --- project/scripts/genDocs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/project/scripts/genDocs b/project/scripts/genDocs index d9ec3ef2f66b..88ec5eaff155 100755 --- a/project/scripts/genDocs +++ b/project/scripts/genDocs @@ -19,7 +19,7 @@ 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 -(cp -vr 0.*/ "$PREVIOUS_SNAPSHOTS_DIR"; true) # Don't fail if no `0.*` found to copy +(cp -vr 3.*/ "$PREVIOUS_SNAPSHOTS_DIR"; true) # Don't fail if no `3.*` found to copy git checkout "$GIT_HEAD" ### Generate the current snapshot of the website ### From 400e4df22cc49b5baf64341294faac5bf4c32268 Mon Sep 17 00:00:00 2001 From: vincenzobaz Date: Wed, 9 Jun 2021 10:42:47 +0200 Subject: [PATCH 2/2] Support both 0.X and 3.X lines --- project/scripts/genDocs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/project/scripts/genDocs b/project/scripts/genDocs index 88ec5eaff155..aa061d59b613 100755 --- a/project/scripts/genDocs +++ b/project/scripts/genDocs @@ -19,7 +19,7 @@ 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 -(cp -vr 3.*/ "$PREVIOUS_SNAPSHOTS_DIR"; true) # Don't fail if no `3.*` found to copy +(cp -vr [03].*/ "$PREVIOUS_SNAPSHOTS_DIR"; true) # Don't fail if no `3.*` found to copy git checkout "$GIT_HEAD" ### Generate the current snapshot of the website ###