Update push.yml

lean-dojo · Dec 6, 2023 · a4217a7 · a4217a7
1 parent dc89243
commit a4217a7
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
@@ -22,7 +22,7 @@ jobs:
       - name: Build project
         run: ~/.elan/bin/lake build
       - name: Download model
-        run: ~/.elan/bin/lake script run LeanCopilot/download
+        run: ~/.elan/bin/lake exe LeanCopilot/download
       - name: Build tests
         run: ~/.elan/bin/lake build LeanCopilotTests
   test_external:
@@ -43,5 +43,5 @@ jobs:
       - name: Build lean4-example
         run: |
           cd lean4-example
-          ~/.elan/bin/lake script run LeanCopilot/download
+          ~/.elan/bin/lake exe LeanCopilot/download
           ~/.elan/bin/lake build