add bash -o pipefail
This commit is contained in:
parent
6775ae17f1
commit
07e9c65861
1 changed files with 1 additions and 1 deletions
2
.github/workflows/build.yml
vendored
2
.github/workflows/build.yml
vendored
|
@ -39,7 +39,7 @@ jobs:
|
|||
|
||||
- name: check file imports
|
||||
run: |
|
||||
env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports
|
||||
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"
|
||||
|
||||
- name: lint HepLean
|
||||
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue