From 98f526640720db5411e0735e6b7e14ff99f4c181 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 21 Mar 2026 17:41:14 +0100 Subject: [PATCH] chore: remove temp bootstrap code (#13021) --- src/Lean/Compiler/InitAttr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index 510846ac3e..6b59f28184 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/src/Lean/Compiler/InitAttr.lean @@ -171,7 +171,7 @@ private unsafe def runInitAttrs (env : Environment) (opts : Options) : IO Unit : -- libraries with their corresponding module in the Environment) must -- first be initialized let pkg? := env.getModulePackageByIdx? modIdx - if env.header.isModule && /- TODO: remove after reboostrap -/ false then + if env.header.isModule then let initializedRuntime ← pure initRuntime <&&> runModInit (phases := .runtime) mod.module pkg? let initializedComptime ← runModInit (phases := .comptime) mod.module pkg? if initializedRuntime || initializedComptime then