diff --git a/STYLE.md b/STYLE.md
index 19380817da..a48c32b9c7 100644
--- a/STYLE.md
+++ b/STYLE.md
@@ -1029,6 +1029,8 @@ The repository contains a file .dir-locals.el in the top-level directory
 which turns on `visual-line-mode` when emacs visits any file in the
 repository.
 
+Documentation can be built locally using `make doc` or `dune build @theories/doc`. The HTML files generated by Dune are placed in `_build/default/HoTT.html/`.
+
 Unfortunately, when viewing source code on Github, these long comment
 lines are not wrapped, making them hard to read.  If you use the
 Stylish plugin, you can make them wrap by adding the following style: