diff options
| author | flip1995 <hello@philkrones.com> | 2020-02-14 12:03:48 +0100 |
|---|---|---|
| committer | flip1995 <hello@philkrones.com> | 2020-02-14 12:03:48 +0100 |
| commit | 0f7918266fa4f4a50237c8bdac79cb1e3001d86c (patch) | |
| tree | b02a278401a0884adff64dcbdc51de47ee164c5b /.github/deploy.sh | |
| parent | 0533cff125d89e15bfda0a265ef01b1b33d8cd95 (diff) | |
Rename current -> stable
Diffstat (limited to '.github/deploy.sh')
| -rw-r--r-- | .github/deploy.sh | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/.github/deploy.sh b/.github/deploy.sh index 8007bc75cdd..b1f572d2b45 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 |