Merge pull request #1186 from HoTT/dependabot/github_actions/Andrew-Chen-Wang/github-wiki-action-5

Bump Andrew-Chen-Wang/github-wiki-action from 4 to 5

Author: mikeshulman

.github/workflows/ci.yml

@@ -57,7 +57,7 @@ jobs:
           publish_dir: "./_www_dir/"
 
       - name: Install gh
-        # Needed for using Andrew-Chen-Wang/github-wiki-action@v4
+        # Needed for using Andrew-Chen-Wang/github-wiki-action@v5
         run: |
           apt-get update
           apt-get install -y gh
@@ -66,6 +66,6 @@ jobs:
         # This step would err if the forked repo does not already have wiki pages.
         # As a workaround, it is disabled for all forked repos.
         if: ${{ github.repository_owner == 'HoTT' && github.ref == 'refs/heads/master' }}
-        uses: Andrew-Chen-Wang/github-wiki-action@v4
+        uses: Andrew-Chen-Wang/github-wiki-action@v5
         with:
           path: _wiki_dir