ci: "head" renamed to "HEAD"

2024-10-30 15:25:33 +01:00
1 parent 26d2fc47f2
commit 185a6d1c1a
@@ -82,4 +82,4 @@ jobs:
      - name: Building docs for a development version
        if: ${{!startsWith(github.event.ref, 'refs/tags/v')}}
        run: |
-          mike deploy --push --update-aliases head latest
+          mike deploy --push --update-aliases HEAD latest