From 8b9fe9b6c2714b51dc8b25c3f90304e488ec29a6 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Sun, 30 Oct 2022 02:52:16 +0200 Subject: [PATCH] doc: fix typo in manual ToC (#1790) There was a typographical error in the manual's table of contents (the section itself and the filename did not have the mistake). --- doc/SUMMARY.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index 5861d2de3f..8974ccee5a 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -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