ci: "dev" renamed to "head" for the latest documentation version

This commit is contained in:
Mateusz Pusz
2024-10-30 14:57:18 +01:00
parent e6443f082d
commit e78a0ac4cf

View File

@ -82,4 +82,4 @@ jobs:
- name: Building docs for a development version - name: Building docs for a development version
if: ${{!startsWith(github.event.ref, 'refs/tags/v')}} if: ${{!startsWith(github.event.ref, 'refs/tags/v')}}
run: | run: |
mike deploy --push --update-aliases dev latest mike deploy --push --update-aliases head latest