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

Add section to README about development of doc-gen4

main
Jeremy Salwen 2023-01-24 18:09:10 -05:00 committed by Henrik Böving
parent 09dbebed9c
commit 7b0ebfa527
1 changed files with 13 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
README.md
View File

@ -14,3 +14,16 @@ lake -Kenv=dev build Test:docs
``` ```
If you have multiple libraries you want to generate documentation for If you have multiple libraries you want to generate documentation for
the recommended way right now is to run it for each library. 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.