Skip to content

Conversation

@Benjamin-Loison
Copy link
Contributor

@Benjamin-Loison Benjamin-Loison commented Jan 14, 2024

Verified exhaustiveness thanks to:

grep -r '```'

@petertodd
Copy link
Member

I'm inclined not to merge this actually, as on github it only makes a difference in one section, and it could be confusing to people reading the file elsewhere without the highlighting.

Anyone else have any thoughts?

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.

3 participants