Lean3 codeblocks open the lean4 web editor

Stream: Zulip meta

[Eric Wieser]

This is marked as lean3:

#check 1

but the link goes to the wrong live editor

[Eric Wieser]

However, the Zulip config looks correct:

image.png

[Eric Wieser]

I think this is probably because Zulip is resolving aliases, but it would be helpful here if it didn't...