From 3c702f38ee1172c40ca09563245a2231db14aef5 Mon Sep 17 00:00:00 2001 From: Jason Yuen Date: Mon, 18 Aug 2025 00:48:05 -0700 Subject: [PATCH] chore: add a missing backtick (#9959) This PR adds a backtick and fixes the docs for `section`. --- src/Lean/Parser/Command.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index de3dbacba0..283442f023 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -259,7 +259,7 @@ def sectionHeader := leading_parser optional ("public ") >> optional ("noncomputable ") /-- -A `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local` +A `section`/`end` pair delimits the scope of `variable`, `include`, `open`, `set_option`, and `local` commands. Sections can be nested. `section ` provides a label to the section that has to appear with the matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the end of the file.