From be1c34fc12619b1690528181179f9c61a6ff026a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 23:05:10 +0200 Subject: [PATCH] chore: README alignment --- README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/README.md b/README.md index d4d135d..75c7ba1 100644 --- a/README.md +++ b/README.md @@ -26,11 +26,14 @@ For example `mathlib4` consists out of 4 modules, the 3 Lean compiler ones and i - `Std` - `Lean` - `Mathlib` + The first build stage is to run doc-gen for all modules separately: + 1. `doc-gen4 single Init` 2. `doc-gen4 single Std` 3. `doc-gen4 single Lean` 4. `doc-gen4 single Mathlib` + 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 here to also generate LeanInk documentation in addition.