Zulip Chat Archive

But, at least in the font I see now, this is not quite orthodox. Someone clearly decided that Bourbaki's version was hard to distinguish from a Z and decided to rotate it.

Patrick Massot (Jul 16 2020 at 09:34):

In the printed book there absolutely no possible confusion because it's too large and bold to be a Z

Mario Carneiro (Jul 16 2020 at 09:35):

Doesn't that imply that lean is dangerous and/or easily misunderstood?

Patrick Massot (Jul 16 2020 at 09:35):

Yes?

Patrick Massot (Jul 16 2020 at 09:35):

How could it be fun otherwise?

Johan Commelin (Jul 16 2020 at 09:35):

Patrick Massot said:

Is that possible?

admins can add emoji

Patrick Massot (Jul 16 2020 at 09:36):

They also changed the menu icon on messages

Anne Baanen (Jul 16 2020 at 09:36):

Hmm, how difficult would it be to hack a font so ':warning:️☡' displays as Knuth's symbol? :thinking:

Patrick Massot (Jul 16 2020 at 09:37):

Knuth's symbol is also deviant. He also clearly thought Bourbaki's symbol looked too much like a Z

Mario Carneiro (Jul 16 2020 at 09:38):

isn't that what the actual "dangerous bend" sign looks like?

Anne Baanen (Jul 16 2020 at 09:38):

We should preface each use of '☡' with '☡' because people might think the dangerous bend symbol looks like '☡'.

Patrick Massot (Jul 16 2020 at 09:39):

Mario, that's the American version

Patrick Massot (Jul 16 2020 at 09:39):

Actually the current French version now looks like a N rather than a Z

Patrick Massot (Jul 16 2020 at 09:40):

Anne Baanen said:

We should preface each use of '☡' with '☡' because people might think the dangerous bend symbol looks like '☡'.

Don't forget the meta keyword then.

Kevin Buzzard (Jul 16 2020 at 09:53):

On the Xena discord, when I made a bunch of students admins, the first thing they did was added loads of extra emojis.

Kevin Buzzard (Jul 16 2020 at 09:53):

We have several Lean emojis

Rob Lewis (Jul 16 2020 at 09:54):

Ah, that image didn't have a transparent background

Kevin Buzzard (Jul 16 2020 at 09:55):

hmmskell.png

Kevin Buzzard (Jul 16 2020 at 09:55):

We have a "hmmskell" emoji

Kevin Buzzard (Jul 16 2020 at 10:00):

If you care about emojis you should switch to discord. We have a stream for cat pictures and everything

Rob Lewis (Jul 16 2020 at 10:00):

Ugh, I hate Gimp, if someone sends me logos/emoji I'll add them but I'm not gonna give that a transparent background myself

Anne Baanen (Jul 16 2020 at 10:03):

Deal. My vacation starts in one week, fear the worst :smiley:

Bhavik Mehta (Jul 16 2020 at 11:41):

Oh yeah I need to make a hmmlean emoji

Kenny Lau (Jul 16 2020 at 18:14):

2020-07-17.png

Kenny Lau (Jul 16 2020 at 18:14):

this is how the tab looks on my side

Kenny Lau (Jul 16 2020 at 18:14):

the number (of new messages) got displaced and is much blurrier

Kenny Lau (Jul 16 2020 at 18:15):

I tried to find a screenshot from before the change happened to no avail

Bryan Gin-ge Chen (Jul 16 2020 at 18:58):

Looks like the new logo is for Zulip 3.0: https://blog.zulip.com/2020/07/16/zulip-3-0-released/

I also noticed the numbers in the favicon looking a lot uglier. I didn't see an issue on their github and don't feel like making one though.

Sebastian Ullrich (Jul 16 2020 at 20:03):

I looked at the new logo for too long and now all I see is a \rightharpoondown and \leftharpoonup

Mario Carneiro (Jul 28 2020 at 08:54):

The logo changed again. Was that our doing?

Johan Commelin (Jul 28 2020 at 08:56):

Hmm, the new is not so readable on a dark background :sad:

Mario Carneiro (Jul 28 2020 at 08:56):

I'm on night mode and I see it in blue in the top left

Mario Carneiro (Jul 28 2020 at 08:57):

are you talking about the emoji?

Rob Lewis (Jul 28 2020 at 08:58):

Everyone has permission to add (and maybe edit?) emoji now

Mario Carneiro (Jul 28 2020 at 08:58):

perhaps that's why all the letter emoji are in big colored boxes

Gabriel Ebner (Jul 28 2020 at 08:58):

No, the Zulip logo has changed.

Gabriel Ebner (Jul 28 2020 at 08:58):

The Z is the ~~mirrored~~ slightly rotated dangerous bend symbol now.

Mario Carneiro (Jul 28 2020 at 08:59):

The emoji question was directed at Johan, not myself :grinning_face_with_smiling_eyes:

Mario Carneiro (Jul 28 2020 at 09:00):

I guess if the ☡ was in a yellow box it would solve the problem

Patrick Massot (Jul 28 2020 at 14:16):

Who changed the logo? I think having two weird Z next to each other feels very weird.

Patrick Massot (Jul 28 2020 at 14:17):

I would rather have the Bourbaki sign replacing the double-harpoon Z and keep a regular Z at the beginning of the Zulip word.

Rob Lewis (Jul 28 2020 at 14:18):

The unicode Bourbaki sign isn't heavy enough to replace the big Z and I wasn't willing to spend the time to make a good looking extra-bold version...

Rob Lewis (Jul 28 2020 at 14:19):

This was just a joke anyway, I was planning to change it back in a few days. If someone wants to make it look good just post an image.

Johan Commelin (Jul 28 2020 at 14:22):

@Rob Lewis I see that you added and , but where is :lean:? The closest I get is :nuclear: (:nuclear:)... :grinning_face_with_smiling_eyes:

Rob Lewis (Jul 28 2020 at 14:23):

Is the "L" favicon the closest we have to a logo?

Johan Commelin (Jul 28 2020 at 14:26):

Probably

Sebastian Ullrich (Jul 28 2020 at 14:48):

You can stack the four letters in the Lean logo and you get, uhhh image.png

Rob Lewis (Jul 28 2020 at 15:22):

Someone should get the Lean one from Kevin's discord.
Kevin Buzzard said:

hmmskell.png

Rob Lewis (Jul 28 2020 at 15:22):

Also :yeet: please.

Patrick Massot (Jul 28 2020 at 15:22):

What does yeet mean?

Gabriel Ebner (Jul 28 2020 at 15:25):

I absolutely loove the colorful leanmoji!

Rob Lewis (Jul 28 2020 at 15:34):

Yeet, a surprisingly clean Urban Dictionary entry!

Alex J. Best (Jul 28 2020 at 15:36):

I guess number 3 is the most reasonable one for the discord emoji

Yeet is a versatile word that can be used as an exclamation, a verb, or even a noun.

As an exclamation it can be used to express excitement, usually happily but also nervously. (See Ex. 1)
It can also be used as an exclamation of victory. (See Ex. 2)
Or as a battle cry or focus-shout while throwing or hitting something, like "HIII-YA". (See Ex. #3)