From 34165f36e6f5e679e1a11b4a8129c7b2fa817bf4 Mon Sep 17 00:00:00 2001 From: tydeu Date: Wed, 23 Aug 2023 14:50:03 -0400 Subject: [PATCH] feat: include Lake as part of the core docs --- DocGen4/Load.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index fc2ef09..619ea7f 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -56,6 +56,6 @@ def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {} def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do - load <| .loadAll [`Init, `Lean] + load <| .loadAll [`Init, `Lean, `Lake] end DocGen4