Skip to content

Commit 09970da

Browse files
committed
remove cache error
1 parent 7f2b713 commit 09970da

File tree

1 file changed

+0
-5
lines changed
  • lean_dojo_v2/lean_dojo/data_extraction

1 file changed

+0
-5
lines changed

lean_dojo_v2/lean_dojo/data_extraction/trace.py

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -152,11 +152,6 @@ def _trace(repo: LeanGitRepo, build_deps: bool) -> None:
152152

153153
with working_directory(repo.name):
154154
# Build the repo using lake.
155-
if not build_deps:
156-
try:
157-
execute("lake exe cache get")
158-
except CalledProcessError:
159-
pass
160155
execute("lake build")
161156

162157
# Copy the Lean 4 stdlib into the path of packages.

0 commit comments

Comments
 (0)