From 0c5c74c02f3ba4a8402e5a807502f9b763de1371 Mon Sep 17 00:00:00 2001 From: rexwzh <1073853456@qq.com> Date: Wed, 11 Sep 2024 09:17:14 +0800 Subject: [PATCH] allow submodule for local type --- src/lean_dojo/data_extraction/lean.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py index 45648d01..ac38ee5f 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