Zulip Chat Archive

Stream: Zulip meta

Topic: linkifier for LTE


view this post on Zulip Johan Commelin (Mar 15 2021 at 17:23):

Can a zulip admin please make liquid#18 link into https://github.com/leanprover-community/lean-liquid/issues/18 ??

view this post on Zulip Rob Lewis (Mar 15 2021 at 17:25):

Does it not already? I think there's a generic linkifier for this. liquid#18

view this post on Zulip Rob Lewis (Mar 15 2021 at 17:26):

Oh, it's lean-liquid#18

view this post on Zulip Johan Commelin (Mar 15 2021 at 17:27):

aah, I didn't know about the generic one

view this post on Zulip Johan Commelin (Mar 15 2021 at 17:27):

I think it's good enough for our needs

view this post on Zulip Johan Commelin (Mar 15 2021 at 17:28):

If people find it too long, we'll bug you to enable lte#18 (-;


Last updated: May 08 2021 at 22:13 UTC