diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py index 0fc7bedb..a359a430 100644 --- a/src/lean_dojo/data_extraction/lean.py +++ b/src/lean_dojo/data_extraction/lean.py @@ -8,7 +8,6 @@ import toml import time import urllib -import shutil import tempfile import webbrowser from enum import Enum @@ -155,10 +154,8 @@ def url_to_repo( repo_name = os.path.basename(url) if repo_type == RepoType.LOCAL: assert is_git_repo(url), f"Local path {url} is not a git repo" - shutil.copytree(url, repo_name) - return Repo(repo_name) - else: - return Repo.clone_from(url, repo_name) + # clone from local path or remote url + return Repo.clone_from(url, repo_name) except Exception as ex: if num_retries <= 0: raise ex