lean: correctly parse expressions nested within attributes by eric-wieser · Pull Request #1817 · pygments/pygments
Navigation Menu
{{ message }}
- Notifications You must be signed in to change notification settings
- Fork 781
Merged
jeanas merged 3 commits intopygments:masterfrom
Apr 20, 2023Merged
lean: correctly parse expressions nested within attributes#1817
jeanas merged 3 commits intopygments:masterfrom
lean: correctly parse expressions nested within attributes#1817
jeanas merged 3 commits intopygments:masterfrom
Conversation
Copy link
Contributor
eric-wieser
commented
May 25, 2021
eric-wieser
commented
This mirrors the syntax fix made in leanprover/vscode-lean#265
eric-wieser added 2 commits
May 25, 2021 17:37eric-wieser commented May 25, 2021
tests/examplefiles/lean/test.lean
Show resolved
Hide resolved
tests/examplefiles/lean/test.lean Show resolved Hide resolved
Copy link
Contributor Author
eric-wieser
commented
May 25, 2021
eric-wieser commented
May 25, 2021CI failure is unrelated to this change.
jeanas approved these changes Mar 8, 2022
Copy link
Contributor
jeanas
left a comment
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.
Anteru
force-pushed
the
master
branch
from
389a55d to
dd52102
Compare
Copy link
Contributor Author
eric-wieser
commented
Apr 12, 2023
eric-wieser commented
Apr 12, 2023Sorry, I totally forgot about this. I've resolved conflicts with the latest master.
eric-wieser
requested a review
from jeanas
jeanas approved these changes Apr 20, 2023
jeanas
merged commit
d5bfdd4
into
pygments:master
Copy link
Contributor
jeanas
commented
Apr 20, 2023
jeanas commented
Apr 20, 2023Thank you!
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
2 participants