Run lean CI in the right directory

trishullab · Jul 22, 2024 · 08344c8 · 08344c8
1 parent 20526e6
commit 08344c8
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
@@ -25,12 +25,15 @@ jobs:
 
     - name: Configure
       run: |
+        cd lean4
         lake exe cache get
 
     - name: Build
       run: |
+        cd lean4
         lake build
 
     - name: Save olean cache
       run: |
+        cd lean4
         lake exe cache pack