Lean playground link dead

Stream: Zulip meta

[Eric Wieser]

The "View in Lean playground" link in this code block is dead

-- click the arrow in the top right

should we just remove it?

[Scott Morrison]

Done.

[Kevin Buzzard]

Works for me: sends me to https://lean.math.hhu.de/#code=--%20click%20the%20arrow%20in%20the%20top%20right%0A or https://leanprover-community.github.io/lean-web-editor/#code=--%20click%20the%20arrow%20in%20the%20top%20right%0A, both of which seem to be working fine. What's the problem here?

[Kevin Buzzard]

-- click the arrow in the top right

[Sebastian Ullrich]

Scott removed a third option linking to leanprover.github.io that was broken