diff --git a/.github/deploy.sh b/.github/deploy.sh index 8007bc75cddd..b1f572d2b455 100644 --- a/.github/deploy.sh +++ b/.github/deploy.sh @@ -11,10 +11,10 @@ cp util/gh-pages/index.html out/master python3 ./util/export.py out/master/lints.json if [[ -n $TAG_NAME ]]; then - echo "Save the doc for the current tag ($TAG_NAME) and point current/ to it" + echo "Save the doc for the current tag ($TAG_NAME) and point stable/ to it" cp -r out/master "out/$TAG_NAME" - rm -f out/current - ln -s "$TAG_NAME" out/current + rm -f out/stable + ln -s "$TAG_NAME" out/stable fi # Generate version index that is shown as root index page diff --git a/util/gh-pages/versions.html b/util/gh-pages/versions.html index a1d385c965aa..cd3611db3005 100644 --- a/util/gh-pages/versions.html +++ b/util/gh-pages/versions.html @@ -64,7 +64,7 @@