push default redirect and add custom title

IDinsight · Aug 13, 2024 · c06f4e0 · c06f4e0
1 parent b48383a
commit c06f4e0
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml
@@ -37,8 +37,9 @@ jobs:
           git fetch origin gh-pages
           mike deploy \
             --push \
+            --title="${{ github.ref_name }} (latest)" \
             --update-aliases ${{ github.ref_name }} latest
-          mike set-default latest
+          mike set-default latest --allow-undefined --push
 
       - name: Add CNAME
         run: |