Merge pull request #173 from eric-wieser/patch-1

Run lean CI in the right directory
trishullab · Jul 23, 2024 · 02ae505 · 02ae505
2 parents 20526e6 + e26f520
commit 02ae505
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
@@ -24,13 +24,16 @@ jobs:
         key: oleans
 
     - name: Configure
+      working-directory: lean4
       run: |
         lake exe cache get
 
     - name: Build
+      working-directory: lean4
       run: |
         lake build
 
     - name: Save olean cache
+      working-directory: lean4
       run: |
         lake exe cache pack