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

fix: ci: use elan's lake to build (for now)

Browse source 
Reason: `leanmake` build is broken due to bad dep inference
This commit is contained in:
tydeu 2021-10-18 13:27:58 -04:00
parent 53ad51e984
commit 44cc860c82
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/ci.yml vendored
View file

@ -53,7 +53,7 @@ jobs:
- name: Check Lean
run: lean --version
- name: Build & Time
run: ./time.sh -j4
run: time lake build
- name: Upload Build
continue-on-error: true
uses: actions/upload-artifact@v2