Skip to content

chore: fix logError interpolation in inlineHtml - #480

Merged
david-christiansen merged 1 commit into
leanprover:mainfrom
b-mehta:html-interpolation-patch
Jul 28, 2025
Merged

chore: fix logError interpolation in inlineHtml#480
david-christiansen merged 1 commit into
leanprover:mainfrom
b-mehta:html-interpolation-patch

Conversation

@b-mehta

@b-mehta b-mehta commented Jul 28, 2025

Copy link
Copy Markdown
Contributor

The string wasn't being interpolated, so error messages were for "{x}" rather than for x itself.

@david-christiansen
david-christiansen merged commit de76a03 into leanprover:main Jul 28, 2025
4 checks passed
@david-christiansen

Copy link
Copy Markdown
Collaborator

Thanks!

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.

2 participants