feat: include Lake as part of the core docs

2023-08-23 14:50:03 -04:00 · 2023-08-23 14:50:03 -04:00 · 34165f36e6
parent a9da3c9e48
commit 34165f36e6
1 changed files with 1 additions and 1 deletions
--- 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