Skip to content

Commit

Permalink
Merge pull request #2109 from Alizter/ps/rr/add_note_about_building_d…
Browse files Browse the repository at this point in the history
…ocumentation_locally_to_style_md

add note about building documentation locally to STYLE.md
  • Loading branch information
Alizter authored Oct 4, 2024
2 parents 6cdd74f + e6aff7c commit f14c526
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions STYLE.md
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down

0 comments on commit f14c526

Please sign in to comment.