max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove unused GH Pages deployment (#3217)

Browse source
This commit is contained in:
Sebastian Ullrich 2024-01-31 11:39:15 +01:00 • committed by GitHub
parent 31981090e4
commit 456e435fe0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
.github/workflows/nix-ci.yml vendored
View file

@ -105,13 +105,6 @@ jobs:
run: |
rm -rf nix-store-cache || true
nix copy ./push-* --to file://$PWD/nix-store-cache?compression=none
- name: Publish manual to GH Pages
uses: peaceiris/actions-gh-pages@v3
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
publish_dir: ./result
destination_dir: ./doc
if: matrix.name == 'Nix Linux' && github.ref == 'refs/heads/master' && github.event_name == 'push'
- id: deploy-info
name: Compute Deployment Metadata
run: |