diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 5483cfe..f0d58bd 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -118,8 +118,6 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String FS.writeFile declarationDataPath json.compress FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec - let root := Id.run <| ReaderT.run (getRoot) config - FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" root) FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs FS.writeFile (basePath / "nav.js") navJs FS.writeFile (basePath / "find" / "find.js") findJs diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 2bae54a..60923d2 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -52,7 +52,6 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath := section Static def styleCss : String := include_str "../../static/style.css" - def siteRootJs : String := include_str "../../static/site-root.js" def declarationDataCenterJs : String := include_str "../../static/declaration-data.js" def navJs : String := include_str "../../static/nav.js" def howAboutJs : String := include_str "../../static/how-about.js" diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 05390fe..c34051d 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -17,7 +17,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do