We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent fdbb94f commit 0856d7bCopy full SHA for 0856d7b
project/scripts/genDocs
@@ -19,7 +19,7 @@ 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
22
-(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
23
git checkout "$GIT_HEAD"
24
25
### Generate the current snapshot of the website ###
0 commit comments