From fed54c2fe8f02838d961dc3002fae895c6c552e9 Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Thu, 19 Sep 2024 03:29:56 +0000 Subject: [PATCH] remove unnecessary line --- src/lean_dojo/data_extraction/trace.py | 1 - 1 file changed, 1 deletion(-) diff --git a/src/lean_dojo/data_extraction/trace.py b/src/lean_dojo/data_extraction/trace.py index eeea2967..379b7bc0 100644 --- a/src/lean_dojo/data_extraction/trace.py +++ b/src/lean_dojo/data_extraction/trace.py @@ -158,7 +158,6 @@ def _trace(repo: LeanGitRepo, build_deps: bool) -> None: cmd = f"lake env lean --threads {NUM_PROCS} --run ExtractData.lean" if not build_deps: cmd += " noDeps" - logger.debug(cmd) execute(cmd, capture_output=True) check_files(packages_path, not build_deps)