Stream: zulip

Topic: Rust code blocks linking to play.rlo


view this post on Zulip pnkfelix (May 05 2021 at 18:27):

I just enabled the zulip setting that makes triple-backquote-rust link to play.rust-lang.org

view this post on Zulip pnkfelix (May 05 2021 at 18:27):

Like so:

fn main() { println!("Hello Zulip People!"); }

view this post on Zulip pnkfelix (May 05 2021 at 18:28):

(ah smart quotes, why?!?) ((fixed in post-edit. but still: why!))

view this post on Zulip pnkfelix (May 05 2021 at 18:29):

(When you hover over Rust code blocks now, it pops up an icon on the right-hand-side; that’s the link to play.rust-lang.org)

view this post on Zulip Jonas Schievink [he/him] (May 05 2021 at 18:34):

oh, neat!

view this post on Zulip hyd-dev (May 05 2021 at 18:36):

I remember that the playground link was available some time ago, but disappeared at some point...

view this post on Zulip Mario Carneiro (May 05 2021 at 18:46):

Speaking of which, did you know you can set the default language for code blocks? Not an admin, but it's at https://rust-lang.zulipchat.com/#organization/organization-settings > Default language for code blocks

view this post on Zulip nikomatsakis (May 05 2021 at 19:18):

woah, that's awesome

view this post on Zulip nikomatsakis (May 05 2021 at 19:18):

Mario Carneiro said:

Speaking of which, did you know you can set the default language for code blocks? Not an admin, but it's at https://rust-lang.zulipchat.com/#organization/organization-settings > Default language for code blocks

hmm, that might make sense :)

view this post on Zulip Pietro Albini (May 05 2021 at 19:20):

that might be annoying for streams like infra though

view this post on Zulip nagisa (May 05 2021 at 19:20):

/me notices an option to allow messages to be deleted too…

view this post on Zulip nagisa (May 05 2021 at 19:21):

right now people have to resort to editing the message to replace it with "(deleted)" or some such.

view this post on Zulip Josh Triplett (May 05 2021 at 19:21):

It'd be nice if default languages could be set per stream.

view this post on Zulip pnkfelix (May 05 2021 at 19:28):

nagisa said:

right now people have to resort to editing the message to replace it with "(deleted)" or some such.

(I didn’t realize that non-admin users lacked that feature)

view this post on Zulip cuviper (May 05 2021 at 23:18):

I think "(deleted)" is what you get when you hit that delete button, unless this has changed

view this post on Zulip cuviper (May 05 2021 at 23:18):

(deleted)

view this post on Zulip cuviper (May 05 2021 at 23:20):

well I don't even see the delete option in my desktop app, but the above just came from deleting on android

view this post on Zulip tmandry (May 06 2021 at 02:59):

I too wish delete was an option

view this post on Zulip tmandry (May 06 2021 at 03:00):

the playground links are great :)


Last updated: Oct 11 2021 at 22:34 UTC