From 116aa1166071c882d369d44e136ee3a252288d2d Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 16 Sep 2024 11:22:26 -0400 Subject: [PATCH] Update informal.lean --- scripts/MetaPrograms/informal.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/MetaPrograms/informal.lean b/scripts/MetaPrograms/informal.lean index 67941bc..13bc985 100644 --- a/scripts/MetaPrograms/informal.lean +++ b/scripts/MetaPrograms/informal.lean @@ -171,6 +171,7 @@ unsafe def importToWebString (i : Import) : MetaM String := do unsafe def main (args : List String) : IO UInt32 := do initSearchPath (← findSysroot) + enableInitializersExecution let mods : Name := `HepLean let imp : Import := {module := mods} let mFile ← findOLean imp.module