From 44cc860c82ccbb60e736dc6a51b48a9d159a8b54 Mon Sep 17 00:00:00 2001 From: tydeu Date: Mon, 18 Oct 2021 13:27:58 -0400 Subject: [PATCH] fix: ci: use elan's `lake` to build (for now) Reason: `leanmake` build is broken due to bad dep inference --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 58dde31628..fa920ff558 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -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