gitja - Set gh-pages host when deploying docs

Commit 1f5b566ef5cff43964c4920cb90192a4ef059a88
Parent: ab15b1d616db83b073ae57ca82ea52ba4a420623
Author: mcol <mcol@posteo.net>
Date: 2021-11-28 16:20:39 +0000
Committer: mcol <mcol@posteo.net>
Committed: 2021-11-28 16:20:39 +0000

Set gh-pages host when deploying docs

.github/workflows/ci.yaml Modified

@@ -37,7 +37,9 @@
         bash test/test.sh
 
     - name: Generate docs
+      if: github.event_name == 'push'
       run: |
+        sed -i 's/localhost:8000/gitserve.mcol.xyz/' config.dhall
         stack run -- -c ./config.dhall -q
 
     - name: Deploy docs