diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index 43ba303528..e3bdbd4949 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -18,4 +18,5 @@ - [Ubuntu Setup](./make/ubuntu-16.04.md) - [macOS Setup](./make/osx-10.9.md) - [Windows Setup](./make/msys2.md) +- [Building This Manual](./mdbook.md) - [Fixing Tests](./fixing_tests.md) diff --git a/doc/mdbook.md b/doc/mdbook.md new file mode 100644 index 0000000000..50240fd9a6 --- /dev/null +++ b/doc/mdbook.md @@ -0,0 +1,14 @@ +This manual is generated by [mdBook](https://github.com/rust-lang/mdBook). We are currently using a +[fork](https://github.com/leanprover/mdBook) of it for the following additional features: + +* Add support for hiding lines in other languages [#1339](https://github.com/rust-lang/mdBook/pull/1339) + +To build this manual, first install the fork via +``` +cargo install --git https://github.com/leanprover/mdBook mdbook +``` +Then use e.g. [`mdbook watch`](https://rust-lang.github.io/mdBook/cli/watch.html) in the `doc/` folder: +``` +cd doc +mdbook watch --open # opens the output in `out/` in your default browser +```