Skip to content

Conversation

lovettchris
Copy link

@lovettchris lovettchris commented Aug 8, 2022

For example, this:

image

Will be tested as the lean code snippet:

image

@Kha
Copy link
Member

Kha commented Aug 9, 2022

It looks like we need rust-lang#1861 in order to placate the CI and future versions of Rust

@lovettchris
Copy link
Author

lovettchris commented Aug 9, 2022

It looks like we need rust-lang#1861 in order to placate the CI and future versions of Rust

Thanks for the links, I merged that fix with this commit https://github.com/lovettchris/mdBook/commit/253add1765a7a0d0e0164a94d353bfecc1f8ffb7 and it seems to be working.

image

@Kha Kha merged commit 9321c10 into leanprover:master Aug 9, 2022
@Kha
Copy link
Member

Kha commented Aug 9, 2022

Thanks!

@lovettchris lovettchris deleted the clovett/fix_nesting branch August 9, 2022 20:36
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