diff --git a/README.md b/README.md index 06cc0dc..e6097cd 100644 --- a/README.md +++ b/README.md @@ -8,6 +8,12 @@ to do this you have to add it to your `lakefile.lean` like this: meta if get_config? env = some "dev" then -- dev is so not everyone has to build it require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" ``` + +Then update your dependencies: +``` +lake -Kenv=dev update +``` + Then you can generate documentation for an entire library using: ``` lake -Kenv=dev build Test:docs @@ -31,4 +37,4 @@ need to serve them from a proper http server for it to work. An easy way to do Note that if you modify the `.js` or `.css` files in doc-gen4, they won't necessarily be copied over when you rebuild the documentation. You can manually copy the changes to the `build/docs` directory to make sure the changes appear, or just do a full recompilation (`lake clean` and `lake build` inside the `doc-gen4` -directory.) \ No newline at end of file +directory.)