Install gh to fix GitHub Actions

HoTT · Jan 9, 2024 · d993b86 · d993b86
1 parent 6913a1a
commit d993b86
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -56,6 +56,10 @@ jobs:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           publish_dir: "./_www_dir/"
 
+      - name: Install gh
+        # Needed for using Andrew-Chen-Wang/github-wiki-action@v4
+        run: sudo apt-get install gh
+
       - name: Push GitHub wiki pages
         # This step would err if the forked repo does not already have wiki pages.
         # As a workaround, it is disabled for all forked repos.