Skip to content

fix: use double backtick code spans for abbreviations containing backticks#709

Merged
mhuisi merged 1 commit into
leanprover:masterfrom
mhuisi:push-uotzrzrontkw
Feb 27, 2026
Merged

fix: use double backtick code spans for abbreviations containing backticks#709
mhuisi merged 1 commit into
leanprover:masterfrom
mhuisi:push-uotzrzrontkw

Conversation

@mhuisi
Copy link
Copy Markdown
Collaborator

@mhuisi mhuisi commented Feb 26, 2026

Abbreviations like `a (for à) were rendered incorrectly in hover tooltips because wrapping them in single backtick code spans caused the inner backtick to prematurely close the span. Use double backtick delimiters when the content contains a backtick, per the CommonMark spec (§6.1).

Closes #708.

…ticks

Abbreviations like \`a (for à) were rendered incorrectly in hover tooltips
because wrapping them in single backtick code spans caused the inner backtick
to prematurely close the span. Use double backtick delimiters when the content
contains a backtick, per the CommonMark spec (§6.1).

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
@mhuisi mhuisi merged commit 011230c into leanprover:master Feb 27, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Grave accent hint interaction with markdown

1 participant