We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
2 parents 6533759 + 400e4df commit c7b89e7Copy full SHA for c7b89e7
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 [03].*/ "$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