Merge pull request #81 from Peiyang-Song/main

Fix CI bug
lean-dojo · May 28, 2024 · f0f8cc4 · f0f8cc4
2 parents 877b768 + 6ab5de9
commit f0f8cc4
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/.github/workflows/push_pr.yml b/.github/workflows/push_pr.yml
@@ -27,7 +27,9 @@ jobs:
       - name: Build project
         run: ~/.elan/bin/lake build
       - name: Download model
-        run: ~/.elan/bin/lake exe LeanCopilot/download
+        run: |
+          export GIT_CLONE_PROTECTION_ACTIVE=false
+          ~/.elan/bin/lake exe LeanCopilot/download
       - name: Build tests
         run: ~/.elan/bin/lake build LeanCopilotTests
   test_external:
@@ -50,5 +52,6 @@ jobs:
       - name: Build lean4-example
         run: |
           cd lean4-example
+          export GIT_CLONE_PROTECTION_ACTIVE=false
           ~/.elan/bin/lake exe LeanCopilot/download
           ~/.elan/bin/lake build