diff --git a/README.md b/README.md
index 643d9d40..a5871875 100644
--- a/README.md
+++ b/README.md
@@ -11,6 +11,16 @@ To build this manual, first install the fork via
 ```bash
 cargo install --git https://github.com/leanprover/mdBook mdbook
 ```
+
+To build a PDF, we use [mdbook-pdf](https://github.com/HollowMan6/mdbook-pdf), which requires Chrome (or Edge on Windows) to be installed first. See the README of mdbook-pdf.
+
+```bash
+cargo install --git https://github.com/HollowMan6/mdbook-pdf.git
+```
+
+and add the appropriate incantations to `book.toml` (as per the mdbook-pdf README).
+
+
 Then use e.g. [`mdbook watch`](https://rust-lang.github.io/mdBook/cli/watch.html) in the root folder:
 ```bash
 mdbook watch --open  # opens the output in `out/` in your default browser
diff --git a/book.pdf b/book.pdf
new file mode 100644
index 00000000..7e4af6ff
Binary files /dev/null and b/book.pdf differ
diff --git a/book.toml b/book.toml
index 4c1e19f5..0f509f41 100644
--- a/book.toml
+++ b/book.toml
@@ -13,3 +13,8 @@ git-repository-url = "https://github.com/leanprover/theorem_proving_in_lean4"
 
 [output.html.playground.boring-prefixes]
 lean = "# "
+
+[output.html.print]
+enable = true
+
+[output.pdf]