Add html creation infrastructure

2021-10-12 17:57:52 +02:00
parent bba062bcc9
commit 517c90704a
3 changed files with 45 additions and 0 deletions
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -51,10 +51,17 @@ jobs:

    - name: create doc
      run: |
+        mkdir -p doc
        cd doc
        nix-shell --run 'make all'
        echo hello world > index.html

+    - name: create atrip.html
+      run: |
+        cd doc
+        nix-shell --run 'make html'
+        mv atrip.html doc/
+
    - name: Deploy
      uses: JamesIves/github-pages-deploy-action@4.1.0
      with: