max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: use enableInitializersExecution at leanpkg

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-16 18:02:51 -07:00
parent a05b7589b5
commit b01239b25b
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Leanpkg.lean
View file

@ -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