Skip to content

Commit

Permalink
ci(deploy_docs.yaml): change latest from alias to identifier
Browse files Browse the repository at this point in the history
  • Loading branch information
Michele-Alberti committed Nov 12, 2024
1 parent a927770 commit 3e2c9c0
Showing 1 changed file with 5 additions and 10 deletions.
15 changes: 5 additions & 10 deletions .github/workflows/deploy_docs.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -49,22 +49,17 @@ jobs:
VERSION="v$MAJOR_MINOR_VERSION"
echo "current version (major-minor): $VERSION"
echo "version=$VERSION" >> $GITHUB_ENV
- name: Set build alias for development
- name: Build and deploy documentation for development
if: github.ref_name == 'development'
run: |
ALIAS=latest
echo "alias: $ALIAS"
echo "alias=$ALIAS" >> $GITHUB_ENV
- name: Set build alias for tagged version
mike deploy --push --update-aliases latest
- name: Build and deploy documentation for tagged version
if: startsWith(github.event.ref, 'refs/tags/v')
run: |
ALIAS=stable
echo "version: $VERSION"
echo "alias: $ALIAS"
echo "alias=$ALIAS" >> $GITHUB_ENV
- name: Build and deploy documentation
# Use mike to deploy the current version of the documentation
# `--push` pushes directly to the gh-pages branch on GitHub
run: mike deploy --push --update-aliases "${{ env.version }}" "${{ env.alias }}"
mike deploy --push --update-aliases "$VERSION" "$ALIAS"
- name: Update default (stable)
if: ${{ env.alias }} == 'stable'
run: mike set-default --push stable

0 comments on commit 3e2c9c0

Please sign in to comment.