From 08344c8c75a9092827a4b618c1b198cc18a0376e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 23 Jul 2024 00:57:47 +0100
Subject: [PATCH] Run lean CI in the right directory

---
 .github/workflows/lean.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
index b39b189d..835df8d6 100644
--- 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