Merge commit 'e181011378' into clippyup

This commit is contained in:
flip1995 2021-11-04 12:52:36 +00:00
commit 4d6c2cce0a
No known key found for this signature in database
GPG key ID: 1CA0DF2AF59D68A5
220 changed files with 3219 additions and 1550 deletions

View file

@ -13,7 +13,8 @@ cp util/gh-pages/lints.json out/master
if [[ -n $TAG_NAME ]]; then
echo "Save the doc for the current tag ($TAG_NAME) and point stable/ to it"
cp -Tr out/master "out/$TAG_NAME"
ln -sf "$TAG_NAME" out/stable
rm -f out/stable
ln -s "$TAG_NAME" out/stable
fi
if [[ $BETA = "true" ]]; then