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.
Last updated: May 02 2025 at 03:31 UTC