max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix typo in manual ToC (#1790)

Browse source 
There was a typographical error in the manual's table of contents (the section itself and the filename did not have the mistake).
This commit is contained in:
David Thrane Christiansen 2022-10-30 02:52:16 +02:00 • committed by GitHub
parent 62ec0bfdb0
commit 8b9fe9b6c2
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/SUMMARY.md
View file

@ -75,7 +75,7 @@
- [Significant Changes from Lean 3](./lean3changes.md)
- [Syntax Highlighting Lean in LaTeX](./syntax_highlight_in_latex.md)
- [User Widgets](examples/widgets.lean.md)
- [Sematic Highlighting](./semantic_highlighting.md)
- [Semantic Highlighting](./semantic_highlighting.md)
# Development