Zulip Chat Archive

Stream: mathlib4

Topic: maintainer merge emoji

Johan Commelin (Mar 12 2025 at 14:33):

Continuing #mathlib4 > Linting space around variables @ 💬

@Michael Rothgang do you have a suggestion for which emoji?

Michael Rothgang (Mar 12 2025 at 15:18):

I do not!

Jeremy Tan (Mar 12 2025 at 17:28):

What about :m:

Michael Rothgang (Mar 12 2025 at 19:22):

Here's a probably horrible idea: :package: as a shorthand for "ship it!".

Michael Rothgang (Mar 12 2025 at 19:23):

Both :construction_worker: and :maintenance: have a good ring to me.

Michael Rothgang (May 02 2025 at 08:26):

#24544 proposes adding :hammer:

Edward van de Meent (May 02 2025 at 08:27):

ban hammer?

Michael Rothgang (May 02 2025 at 08:27):

judge's hammer?

Kevin Buzzard (May 02 2025 at 10:28):

Sledgehammer?

Michael Rothgang (May 02 2025 at 15:18):

Status update: this is live and "works", but it exposed a pre-existing assumption in the emojibot, which is no longer true. How should a PR be labelled which has multiple emoji-worthy labels? (The current code picks one.)

Last updated: Dec 20 2025 at 21:32 UTC