From b01239b25b2f3e461b272aef0e6f5c0ae9eb09de Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Aug 2021 18:02:51 -0700 Subject: [PATCH] fix: use `enableInitializersExecution` at `leanpkg` --- src/Leanpkg.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean index c43ba47313..3be55008de 100644 --- a/src/Leanpkg.lean +++ b/src/Leanpkg.lean @@ -219,6 +219,7 @@ end Leanpkg def main (args : List String) : IO UInt32 := do try + Lean.enableInitializersExecution Lean.initSearchPath none -- HACK let (cmd, outerArgs, innerArgs) ← Leanpkg.splitCmdlineArgs args Leanpkg.main cmd outerArgs innerArgs