remove unnecessary line

lean-dojo · Sep 19, 2024 · fed54c2 · fed54c2
1 parent 7f66e93
commit fed54c2
Showing 1 changed file with 0 additions and 1 deletion.
diff --git 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)