diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index c69fc5af9e..b36709cc7f 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -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) diff --git a/doc/dev/bootstrap.md b/doc/dev/bootstrap.md index bc2287730a..d8a2782059 100644 --- a/doc/dev/bootstrap.md +++ b/doc/dev/bootstrap.md @@ -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/`. \ No newline at end of file +version in `src/`.