There was an error while loading. Please reload this page.
1 parent 527c864 commit ed11e3fCopy full SHA for ed11e3f
1 file changed
README.md
@@ -59,10 +59,13 @@ arrange for them to target the correct versions of Lean. To test these
59
links locally, follow the instructions in a comment in the definition
60
of `staticJs` in `Main.lean`.
61
62
-To build the manual, run the following command:
+The manual and tutorials site contain circular cross-references, so
63
+building them requires first discovering the valid targets for both
64
+and then generating both sites' HTML. To build the HTML, run the
65
+following shell script:
66
67
```
-lake exe generate-manual --depth 2
68
+./generate-html.sh
69
70
71
Then run a local web server on its output:
0 commit comments