Amend the documentation build (#34)

2025-08-10 18:55:45 +08:00
parent 24d590f4ea
commit 9d4bfec43f
1 changed files with 3 additions and 2 deletions
@@ -51,9 +51,10 @@ jobs:
      - name: Deploy versioned docs
        if: startsWith(github.ref, 'refs/tags/')
        run: |
-          mike deploy --push --update-aliases ${{ steps.version.outputs.version }} latest
+          mike deploy --push --update-aliases ${{ steps.version.outputs.version }} stable

      - name: Deploy dev docs
        if: github.ref == 'refs/heads/main'
        run: |
-          mike deploy --push dev
+          mike deploy --push latest
+          mike set-default --push latest