Zulip Chat Archive

Stream: new members

Topic: octopus


view this post on Zulip Paul van Wamelen (Jun 02 2020 at 20:53):

I can't stand it anymore! What does it mean when people add an :octopus: to a message? (I have a friend that likes to say: "well, that has tentacles...", but it doesn't seem to be how people use :octopus: here.)

view this post on Zulip Marc Huisinga (Jun 02 2020 at 20:56):

i've asked the same question a while back: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20nightly/near/193059045

view this post on Zulip Mario Carneiro (Jun 02 2020 at 20:58):

I think part of it is that it inexplicably shows up in the popular list, although at this point I wouldn't be surprised if that is quite accurate

view this post on Zulip Reid Barton (Jun 02 2020 at 21:07):

It's sort of an unofficial Zulip logo I think.

view this post on Zulip Reid Barton (Jun 02 2020 at 21:08):

at least, that's the reason it's on the Popular list (which I think is just hard-coded)

view this post on Zulip Mario Carneiro (Jun 02 2020 at 21:14):

https://github.com/zulip/zulip/blob/b019d7ffe82e27d2cde0ee0bceda19560c93639d/static/shared/js/typeahead.js#L1-L29

view this post on Zulip Pedro Minicz (Jun 06 2020 at 04:44):

Okay, this is the best thread I've seen here thus far.


Last updated: May 13 2021 at 21:12 UTC