Improve installation instructions

main
Denis Gorbachev 2023-05-26 15:05:21 +07:00 committed by Henrik Böving
parent e0eecc3334
commit b91272c643
1 changed files with 7 additions and 1 deletions

View File

@ -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 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" 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: Then you can generate documentation for an entire library using:
``` ```
lake -Kenv=dev build Test:docs lake -Kenv=dev build Test:docs