Emoji reactions

Stream: general

[Damiano Testa]

Kyle Miller said:

(Damiano Testa Could the pr/issue emoji bot also add emojis to the first message in a topic whose name contains a pr/issue number?)

This just got merged: if everything goes as planned, the emoji reactions associated to the PR status stay as they were, except that the first message in each thread in #**PR reviews> that mentions the PR number behaves as though it contained the PR number.

[Damiano Testa]

Thus, while I would still encourage everyone to provide an explicit link to the PR in each #**PR reviews> thread, the first message should receive emoji updates regardless of whether it contains the PR number in its text.

[Damiano Testa]

As with all new automation, please let me know if you notice regressions or non-progressions! :smile:

[Joscha Mennicken]

Just curious: Is the list of emojis and their meanings documented somewhere except in the bot's source code itself? I didn't find any docs in a quick search.

[Damiano Testa]

I don't think that it is officially documented anywhere, but these are the ones that I can think of:

PR status	Emoji
Maintainer merged	:hammer:
Sent to bors
Merged
Awaiting author	:writing:
Closed
Delegated	:victory:

[Joscha Mennicken]

Reading through the source code, your list seems to be comprehensive. I've also found a complete description in the scripts readme under the section API surrounding CI.

[Jeremy Tan]

What was the emoji originally meant for?

[Aaron Liu]

nhab ehcstued

[Aaron Liu]

deutsche bahn

[Jeremy Tan]

No – I meant the purpose of that emoji

[Aaron Liu]

great question

[Aaron Liu]

I found #condensed mathematics > The elephant in the room @ 💬

[Jeremy Tan]

Also for and

[Jeremy Tan]

We should also replace with the new Rocq logo (and move or add the code :rocq:)

[Johan Commelin]

I think might have been used by some bot, during the port? I don't remember the details...

[Johan Commelin]

is the platonic ideal of a concept that some people love and can't comprehend why others do not, whereas others hate it and can't comprehend why others do not.

You can guess in which camp I am :smiley: