r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix: links in search

main
Henrik Böving 2022-04-07 12:44:33 +02:00
parent 06c20ee46f
commit 67402506c7
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
DocGen4/Output.lean
View File

@ -94,7 +94,7 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
for (_, mod) in result.moduleInfo.toArray do for (_, mod) in result.moduleInfo.toArray do
for decl in filterMapDocInfo mod.members do for decl in filterMapDocInfo mod.members do
let name := decl.getName.toString let name := decl.getName.toString
let config := { config with depthToRoot := 2 } let config := { config with depthToRoot := 0 }
let doc := decl.getDocString.getD "" let doc := decl.getDocString.getD ""
let root := Id.run <| ReaderT.run (getRoot) config let root := Id.run <| ReaderT.run (getRoot) config
let link := root ++ s!"../semantic/{decl.getName.hash}.xml#" let link := root ++ s!"../semantic/{decl.getName.hash}.xml#"

2
static/search.js
View File

@ -96,7 +96,7 @@ function handleSearch(dataCenter, err, ev) {
const d = sr.appendChild(document.createElement("a")); const d = sr.appendChild(document.createElement("a"));
d.innerText = name; d.innerText = name;
d.title = name; d.title = name;
d.href = docLink; d.href = SITE_ROOT + docLink;
} }
} }
// handle error // handle error