Hotfix: fetch gh-pages before running mike

Author: pingelit

.github/workflows/doc-pub.yml

@@ -38,6 +38,7 @@ jobs:
     - name: Deploy release version using mike
       if: startsWith(github.ref, 'refs/tags/v')
       run: |
+          git fetch origin gh-pages --depth=1
           version=${GITHUB_REF##*/}
           echo "Deploying release version $version"
           mike deploy "$version" latest --update-aliases --push