From 7b0ebfa52787d68bd51f2b11b91a85a1fa13e130 Mon Sep 17 00:00:00 2001 From: Jeremy Salwen Date: Tue, 24 Jan 2023 18:09:10 -0500 Subject: [PATCH] Add section to README about development of doc-gen4 --- README.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/README.md b/README.md index 73b2015..e2ab4e0 100644 --- a/README.md +++ b/README.md @@ -14,3 +14,16 @@ lake -Kenv=dev build Test:docs ``` If you have multiple libraries you want to generate documentation for the recommended way right now is to run it for each library. + +## Development of doc-gen4 +You can build docs using a modified `doc-gen4` as follows: Replace the `from git "..." @ "main"` in the `lakefile.lean` with just `from "..."` using the path to the modified version of `doc-gen4`. E.g. if the +path to the modified version of `doc-gen4` is `../doc-gen4`, it would be: +``` +meta if get_config? env = some "dev" then -- dev is so not everyone has to build it +require «doc-gen4» from "../doc-gen4" +``` + +The root of the built docs will be `build/docs/index.html`. However, due to the "Same Origin Policy", the +generated website will be partially broken if you just open the generated html files in your browser. You +need to serve them from a proper http server for it to work. An easy way to do that is to run +`python3 -m http.server` from the `build/docs` directory. \ No newline at end of file