Skip to content

lean: correctly parse expressions nested within attributes#1817

Merged
jeanas merged 3 commits intopygments:masterfrom
eric-wieser:lean-binders
Apr 20, 2023
Merged

lean: correctly parse expressions nested within attributes#1817
jeanas merged 3 commits intopygments:masterfrom
eric-wieser:lean-binders

Conversation

@eric-wieser
Copy link
Contributor

This mirrors the syntax fix made in leanprover/vscode-lean#265

@eric-wieser
Copy link
Contributor Author

CI failure is unrelated to this change.

Copy link
Contributor

@jeanas jeanas left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Could you rebase this on top of master? There was a breaking change in the CI.

@jeanas jeanas added the update needed Waiting for an update from the PR/issue creator label Mar 16, 2022
@eric-wieser
Copy link
Contributor Author

Sorry, I totally forgot about this. I've resolved conflicts with the latest master.

@eric-wieser eric-wieser requested a review from jeanas April 12, 2023 22:45
@jeanas jeanas removed the update needed Waiting for an update from the PR/issue creator label Apr 20, 2023
@jeanas jeanas merged commit d5bfdd4 into pygments:master Apr 20, 2023
@jeanas
Copy link
Contributor

jeanas commented Apr 20, 2023

Thank you!

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