pr emoji

Stream: Zulip meta

[Matthew Ballard]

Is there a "PR submitted" emoji?

[Johan Commelin]

Not yet. Feel free to add it (-;

[Matthew Ballard]

It seems that this is canonical one.

[Matthew Ballard]

I lack permissions to add it.

[Johan Commelin]

@Matthew Ballard Done :wink:

[Mario Carneiro]

The icon is squahed

[Mario Carneiro]

also I would suggest making it purple like github's

[Mario Carneiro]

black on transparent is terrible for dark mode users

[Kyle Miller]

How is this one?

It's the open pull request icon from GitHub

[Mario Carneiro]

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

[Johan Commelin]

I agree that it looks better.

[Johan Commelin]

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

[Matthew Ballard]

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

[Adam Topaz]

I think the emoji would suffice for that?

[Matthew Ballard]

That is merged though

[Matthew Ballard]

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

[Matthew Ballard]

Like this

[Alex J. Best]

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]

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

[Damiano Testa]

Matthew Ballard said:

Like this

Screen Shot 2022-08-05 at 10.58.18 AM.png

Would it be possible to add this emoji?

For context, I am planning to expand the automated emoji reactions on PRs that have been closed and not merged, so that the bot will post this icon on messages that mention the PR.

[Damiano Testa]

I don't mind the name, but I can suggest :closed-pr:, for inspiration! :smile:

It is the name that I used in #20902.

[Johan Commelin]

[Eric Wieser]

Can I tempt someone into making a non-ugly transparent one?

[Damiano Testa]

I kind of agree with Kim that the emoji is not very pretty (although I find the emoji for :ugly: very inappropriate!).

[Damiano Testa]

What about using :broken_heart: ? Or something else that is already available?

[Kim Morrison]

The new emoji would be great if it were transparent (or even if it just didn't touch the top and right edges).

[Kim Morrison]

(Separately, I'd be happy to learn what's wrong with the :ugly: emoji, I feel I must be missing some cultural knowledge. :-)

[Damiano Testa]

Here is an attempt at manually making the background transparent.

Screen Shot 2022-08-05 at 10.58.18 AM_2.png

[Damiano Testa]

Wrt to ugly duckling, I think that it is more of a personal view, than cultural knowledge.

I never liked the story and I always felt there must be better ways to learn about bullying and physical differences! :upside_down:

[Eric Wieser]

You could start over with https://primer.style/foundations/icons/git-pull-request-closed-16 and draw a red circle under it

[Eric Wieser]

Or just recolor it to red

[Damiano Testa]

I don't feel that I am very good at this...

imageedit_8_6513378514.png

[Eric Wieser]

The trick is to modify the SVG then save to PNG, not save to PNG then recolor

[Damiano Testa]

Well, what I did was take a screenshot of the image you linked and then googled for "change color in a picture".

[Damiano Testa]

When I copy the SVG, I get something that looks like HTML: I do not know how to convert that to something that I can edit...

[Julian Berman]

https://www.vectorpea.com/

[Damiano Testa]

Untitled-11.png

[Damiano Testa]

Thanks Julian! My best attempt so far...

[Damiano Testa]

While the discussion about the emoji rages, the PR got merged. Let's see if the action works.

I am going to use #20750 as a test: I will close it, and let's see if the bot flags it as closed!

[Damiano Testa]

It worked!

[Damiano Testa]

I will now create a PR that removes the reaction, in case the PR gets re-opened, since I had forgotten about this eventuality.

[Damiano Testa]

Meanwhile, I would be happy for some help with the emoji, since the current one does not seem satisfactory! :smile:

[Johan Commelin]

[Damiano Testa]

Thanks, Johan this is much nicer than my attempts!!

[Damiano Testa]

By the way, #20941 contains a correction to the script that removes the reaction, when the PR is reopened, in case someone feels like merging it... :smile:

(I'll include a link to the test PR for closure, to see the interaction: do not merge this #20750!)

[Damiano Testa]

I hope that #20942 is the last iteration.

The new emoji has the same name, but different emoji_code! So, the script now adds the new emoji, but removes theold one (as you can see from the comment above, where there is only the new closed-pr emoji).

#20942 uses the new emoji_code, so that the script should now add and remove the correct emoji!

[Damiano Testa]

It works as intended now!

[Damiano Testa]

Well, that only took 5 PRs and two changes to the local emojis. :man_facepalming:

[Kevin Buzzard]

I can't really see the merge emoji in dark mode btw ;-)

[Kevin Buzzard]

Screenshot_20250122-105610_Zulip.png

[Damiano Testa]

Kevin, I'm sure that 7 PRs and 4 emoji changes on Zulip can fix that.