Zulip Chat Archive

Stream: Zulip meta

Topic: pr emoji

Matthew Ballard (Aug 03 2022 at 19:34):

Is there a "PR submitted" emoji?

Johan Commelin (Aug 04 2022 at 05:26):

Not yet. Feel free to add it (-;

Matthew Ballard (Aug 04 2022 at 18:07):

It seems that this is canonical one.

Matthew Ballard (Aug 04 2022 at 18:07):

I lack permissions to add it.

Johan Commelin (Aug 05 2022 at 04:37):

@Matthew Ballard Done :pull-request: :pull-request: :pull-request: :pull-request: :wink:

Mario Carneiro (Aug 05 2022 at 04:49):

The icon is squahed

Mario Carneiro (Aug 05 2022 at 04:49):

also I would suggest making it purple like github's

Mario Carneiro (Aug 05 2022 at 04:50):

black on transparent is terrible for dark mode users

Kyle Miller (Aug 05 2022 at 04:59):

How is this one? :pr-open:

It's the open pull request icon from GitHub

Mario Carneiro (Aug 05 2022 at 05:03):

github dark mode uses #3fb950 on transparent, does that work on light too?

Johan Commelin (Aug 05 2022 at 05:04):

I agree that it looks better.

Johan Commelin (Aug 05 2022 at 05:04):

I'll delete mine, and free up the :pull-request: emoji tag.

Matthew Ballard (Aug 05 2022 at 14:30):

A natural question: should the closed PR emoji also be added?

Adam Topaz (Aug 05 2022 at 14:51):

I think the :merge: emoji would suffice for that?

Matthew Ballard (Aug 05 2022 at 14:56):

That is merged though

Matthew Ballard (Aug 05 2022 at 14:56):

Like oh I need to work more on this PR so I am closing it for now.

Matthew Ballard (Aug 05 2022 at 14:58):

Like this

Alex J. Best (Aug 05 2022 at 15:00):

People tend not to do that on the mathlib GitHub for whatever reason (maybe they still want ci to make oleans for them) it's far more common to just mark a pr as WIP, or needs-work or needs-adoption or some such.

Eric Wieser (Aug 16 2022 at 12:47):

Perhaps we can ask Zulip to allow separate images for dark/light mode emojis?

Last updated: Dec 20 2023 at 11:08 UTC