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