diff --git a/README.md b/README.md index ca3a26d..02ed982 100644 --- a/README.md +++ b/README.md @@ -11,18 +11,19 @@ require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" Then update your dependencies: ``` -lake -Kenv=dev update +lake -R -Kenv=dev update ``` Then you can generate documentation for an entire library and all files imported by that library using: ``` -lake -Kenv=dev build Test:docs +lake -R -Kenv=dev build Test:docs ``` If you have multiple libraries you want to generate full documentation for: ``` -lake -Kenv=dev build Test:docs Foo:docs +lake -R -Kenv=dev build Test:docs Foo:docs ``` + Note that `doc-gen4` currently always generates documentation for `Lean`, `Init` and `Lake` in addition to the provided targets. diff --git a/test_docs.sh b/test_docs.sh index 387af03..c42005e 100755 --- a/test_docs.sh +++ b/test_docs.sh @@ -9,5 +9,5 @@ set -x cd "$1" sed -i "s|from git \"https://github.com/leanprover/doc-gen4\" @ \"main\"| from \"..\" / \"doc-gen4\" with NameMap.empty|" lakefile.lean -lake -Kdoc=on update -lake -Kdoc=on build Std:docs +lake -R -Kdoc=on update +lake -R -Kdoc=on build Std:docs