Update __init__.py

lean-dojo · Jul 23, 2024 · 042452c · 042452c
1 parent 2ff92a4
commit 042452c
Showing 1 changed file with 0 additions and 5 deletions.
diff --git a/src/lean_dojo/__init__.py b/src/lean_dojo/__init__.py
@@ -28,8 +28,3 @@
 from .interaction.parse_goals import Declaration, Goal, parse_goals
 from .data_extraction.lean import get_latest_commit, LeanGitRepo, LeanFile, Theorem, Pos
 from .constants import __version__
-
-if os.geteuid() == 0:
-    logger.warning(
-        "Running LeanDojo as the root user may cause unexpected issues. Proceed with caution."
-    )