Zulip Chat Archive

Stream: Zulip meta

Topic: Live button

Gabriel Ebner (May 07 2021 at 08:11):

There used to be a button on every code block to open it in the javascript version of Lean. Does anybody know what happened to it?

#eval "hello, world"

Mario Carneiro (May 07 2021 at 08:13):

the same thing happened on the rust zulip recently. Maybe zulip changed their API and lost the settings?

Julian Berman (May 07 2021 at 13:28):

Probably it's related to https://github.com/zulip/zulip/pull/18212

Julian Berman (May 07 2021 at 13:28):

Which says amusingly:

(Though we'll want to also do some communication with the Lean/Rust communities).

Julian Berman (May 07 2021 at 13:30):

Maybe the fix is now the Lean playground isn't hardcoded in the Zulip codebase and someone just needs to configure it specifically for this one in the Settings pane?

Mario Carneiro (May 07 2021 at 13:42):

Ah, perfect. Indeed the old settings were in the PR, so I copied those into the new settings menu and things should be working.

def zulip := "fancy"

Eric Wieser (May 07 2021 at 13:50):

After refreshing it works on Gabriel's message too. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC