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

chore: CI: continue on test-summary failure

Browse source
This commit is contained in:
Sebastian Ullrich 2024-03-27 14:03:10 +01:00 • committed by GitHub
parent 94d6286e5a
commit 3ee1cdf3de
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -83,6 +83,7 @@ jobs:
with:
paths: push-test/test-results.xml
if: always()
continue-on-error: true
- name: Build manual
run: |
nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc