Skip to content

Commit

Permalink
Merge pull request #62 from emilyriehl/render-styleguide
Browse files Browse the repository at this point in the history
Render STYLEGUIDE on the website
  • Loading branch information
fizruk authored Dec 11, 2023
2 parents 4c0972e + 642f460 commit a8f1443
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 0 deletions.
4 changes: 4 additions & 0 deletions mkdocs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ docs_dir: src
nav:
- About:
- index.md
- Code style: STYLEGUIDE.md
- Other Yoneda formalizations: other.md

- HoTT:
Expand Down Expand Up @@ -38,6 +39,9 @@ markdown_extensions:
- admonition
- footnotes
- pymdownx.details
- pymdownx.tasklist
- pymdownx.snippets:
check_paths: true
- mdx_math
- pymdownx.highlight:
anchor_linenums: true
Expand Down
1 change: 1 addition & 0 deletions src/STYLEGUIDE.md
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
--8<-- "STYLEGUIDE.md"

0 comments on commit a8f1443

Please sign in to comment.