Zulip Chat Archive

Stream: general

Topic: Lean's syntax highlighter breaks github's blame


view this post on Zulip Eric Wieser (Dec 14 2020 at 16:28):

Anyone seen this before?

https://github.com/leanprover-community/mathlib/blame/c722b967980e29ffbf6ef8db4ed200d22de75c9f/src/data/fintype/basic.lean#L200

view this post on Zulip Kevin Buzzard (Dec 14 2020 at 16:33):

I'm pretty sure it didn't used to

view this post on Zulip Eric Wieser (Dec 14 2020 at 16:33):

I filed a ticket with github

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 14 2020 at 17:39):

Oh yeah, this is just all blame views, not a lean issue

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Dec 14 2020 at 18:50):

It got acknowledged at least.

view this post on Zulip Floris van Doorn (Dec 15 2020 at 00:05):

The issue seems to be fixed (at least, I don't see anything weird).

view this post on Zulip 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: May 13 2021 at 19:20 UTC