From 67402506c7e37c32c6df4d7661fc025a29b9cbfb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 7 Apr 2022 12:44:33 +0200
Subject: [PATCH] fix: links in search

---
 DocGen4/Output.lean | 2 +-
 static/search.js    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index f0d58bd..ba53d21 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -94,7 +94,7 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
   for (_, mod) in result.moduleInfo.toArray do
     for decl in filterMapDocInfo mod.members do
       let name := decl.getName.toString
-      let config := { config with depthToRoot := 2 }
+      let config := { config with depthToRoot := 0 }
       let doc := decl.getDocString.getD ""
       let root := Id.run <| ReaderT.run (getRoot) config
       let link :=  root ++ s!"../semantic/{decl.getName.hash}.xml#"
diff --git a/static/search.js b/static/search.js
index 5b075de..074d8bc 100644
--- a/static/search.js
+++ b/static/search.js
@@ -96,7 +96,7 @@ function handleSearch(dataCenter, err, ev) {
       const d = sr.appendChild(document.createElement("a"));
       d.innerText = name;
       d.title = name;
-      d.href = docLink;
+      d.href = SITE_ROOT + docLink;
     }
   }
   // handle error