From 0b520102914e6072aa12d21a64e098ee0d920dcf Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Tue, 29 Aug 2023 17:45:58 -0400
Subject: [PATCH] fix: source links for Lake

---
 DocGen4/Output/SourceLinker.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean
index 676fb30..48ca406 100644
--- a/DocGen4/Output/SourceLinker.lean
+++ b/DocGen4/Output/SourceLinker.lean
@@ -86,6 +86,8 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange 
     let root := module.getRoot
     let basic := if root == `Lean ∨ root == `Init then
       s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
+    else if root == `Lake then
+      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/lake/{path}.lean"
     else
       match ws.packageArray.find? (·.isLocalModule module) with
       | some pkg =>