Zulip Chat Archive
Stream: general
Topic: Lean's syntax highlighter breaks github's blame
Eric Wieser (Dec 14 2020 at 16:28):
Anyone seen this before?
Kevin Buzzard (Dec 14 2020 at 16:33):
I'm pretty sure it didn't used to
Eric Wieser (Dec 14 2020 at 16:33):
I filed a ticket with github
Bryan Gin-ge Chen (Dec 14 2020 at 17:14):
At least one other person has this issue: https://github.community/t/github-blame-view-shows-html-markup/149818
Eric Wieser (Dec 14 2020 at 17:39):
Oh yeah, this is just all blame views, not a lean issue
Kevin Buzzard (Dec 14 2020 at 18:39):
that's good news because it means it'll be fixed quicker. Did Reid's weird Lean display bug ever get fixed?
Eric Wieser (Dec 14 2020 at 18:50):
It got acknowledged at least.
Floris van Doorn (Dec 15 2020 at 00:05):
The issue seems to be fixed (at least, I don't see anything weird).
Bryan Gin-ge Chen (Dec 15 2020 at 00:11):
Yep, looks like it was fixed about 3 hours ago: https://github.community/t/github-blame-view-shows-html-markup/149818/3
Last updated: Dec 20 2023 at 11:08 UTC