ci: create hosts before push

MartinBernstorff · Oct 27, 2023 · 6d38c59 · 6d38c59
1 parent 357ac0a
commit 6d38c59
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
@@ -26,6 +26,11 @@ jobs:
           registry: ghcr.io
           username: MartinBernstorff
           password: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Create github hosts file
+        run: | # If this file is not created, the dev container fails because of non-existant mount
+          mkdir -p ~/.config/gh
+          touch ~/.config/gh/hosts.yml
 
       - name: Pre-build dev container image
         uses: devcontainers/[email protected]