max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: include missing chapter

Browse source
This commit is contained in:
Sebastian Ullrich 2022-04-04 17:56:19 +02:00
parent 6aee3fb304
commit adcdd16d7a
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
doc/SUMMARY.md
View file

@ -60,6 +60,7 @@
# Development
- [Development Guide](./dev/index.md)
- [Bootstrapping](./dev/bootstrap.md)
- [Commit Convention](./dev/commit_convention.md)
- [Building Lean](./make/index.md)
- [Ubuntu Setup](./make/ubuntu.md)

3
doc/dev/bootstrap.md
View file

@ -1,4 +1,3 @@
# Lean Build Bootstrapping
Since version 4, Lean is a partially bootstrapped program: most parts of the
@ -119,4 +118,4 @@ affect later stages. This is an issue in two specific cases.
To modify either of these flags both for building and editing the stdlib, adjust
the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset
on the next `update-stage0` when the file is overwritten with the original
version in `src/`.
version in `src/`.