Zulip Chat Archive
Stream: new members
Topic: octopus
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.)
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
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
Reid Barton (Jun 02 2020 at 21:07):
It's sort of an unofficial Zulip logo I think.
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)
Mario Carneiro (Jun 02 2020 at 21:14):
Pedro Minicz (Jun 06 2020 at 04:44):
Okay, this is the best thread I've seen here thus far.
Last updated: Dec 20 2023 at 11:08 UTC