minor fix

lean-dojo · Feb 23, 2024 · 9056052 · 9056052
1 parent a1f32c8
commit 9056052
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py
@@ -519,7 +519,7 @@ def get_dependencies(
             for name, repo in self._parse_lakefile_dependencies(lakefile["content"]):
                 if name not in deps:
                     deps[name] = repo
-                for dd_name, dd_repo in repo._get_lean4_dependencies().items():
+                for dd_name, dd_repo in repo.get_dependencies().items():
                     deps[dd_name] = dd_repo
 
         return deps