feat: Build only HepLean

This commit is contained in:
jstoobysmith 2024-05-14 10:47:04 -04:00
parent 2b18ccb8fe
commit 2be61744cb

View file

@ -38,7 +38,7 @@ jobs:
with:
linters: gcc
run: |
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI HepLean | tee stdout.log"
- name: lint HepLean
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}