Update doc

This commit is contained in:
Alejandro Gallo 2021-09-06 18:34:54 +02:00
parent 0d926aa618
commit 7cddf4735f

View File

@ -41,8 +41,9 @@ jobs:
- name: create doc - name: create doc
run: | run: |
cd doc && nix-shell --run 'make all' cd doc
cd doc && echo hello world > index.html nix-shell --run 'make all'
echo hello world > index.html
- name: Deploy - name: Deploy
uses: JamesIves/github-pages-deploy-action@4.1.0 uses: JamesIves/github-pages-deploy-action@4.1.0