From ac0d0ab32d2eccb3bd1ca4d0f93c5d78a50452ac Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 30 Oct 2020 15:59:56 +0100 Subject: [PATCH] doc: document documentation build, mention fork --- doc/SUMMARY.md | 1 + doc/mdbook.md | 14 ++++++++++++++ 2 files changed, 15 insertions(+) create mode 100644 doc/mdbook.md 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 +```