Install gh to fix GitHub Actions (3rd try)

HoTT · Jan 9, 2024 · a05b0e4 · a05b0e4
1 parent a1cf8b3
commit a05b0e4
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -58,7 +58,9 @@ jobs:
 
       - name: Install gh
         # Needed for using Andrew-Chen-Wang/github-wiki-action@v4
-        run: apt-get install gh
+        run: |
+          apt-get update
+          apt-get install -y gh
 
       - name: Push GitHub wiki pages
         # This step would err if the forked repo does not already have wiki pages.