chore: README alignment

main
Henrik Böving 2022-07-21 23:05:10 +02:00
parent 0cff3d7cda
commit be1c34fc12
1 changed files with 3 additions and 0 deletions

View File

@ -26,11 +26,14 @@ For example `mathlib4` consists out of 4 modules, the 3 Lean compiler ones and i
- `Std` - `Std`
- `Lean` - `Lean`
- `Mathlib` - `Mathlib`
The first build stage is to run doc-gen for all modules separately: The first build stage is to run doc-gen for all modules separately:
1. `doc-gen4 single Init` 1. `doc-gen4 single Init`
2. `doc-gen4 single Std` 2. `doc-gen4 single Std`
3. `doc-gen4 single Lean` 3. `doc-gen4 single Lean`
4. `doc-gen4 single Mathlib` 4. `doc-gen4 single Mathlib`
Note that you can also just make a call to submodules so `Mathlib.Algebra` Note that you can also just make a call to submodules so `Mathlib.Algebra`
will work standalone as well. Furthermore one can use the `--ink` flag will work standalone as well. Furthermore one can use the `--ink` flag
here to also generate LeanInk documentation in addition. here to also generate LeanInk documentation in addition.