Zulip Chat Archive

Stream: general

Topic: Bors closing PR

Yaël Dillies (Oct 26 2021 at 20:29):

Bors just closed #9980 with a purple tick. Is it something new?

Patrick Stevens (Oct 26 2021 at 20:33):

The first Bors merge PR is https://github.com/leanprover-community/mathlib/pull/768 which also has a purple tick

Bryan Gin-ge Chen (Oct 26 2021 at 20:42):

My guess is GitHub changed something in their UI.

Alex J. Best (Oct 26 2021 at 20:42):

They all have purple ticks now it seems?

Yaël Dillies (Oct 26 2021 at 20:43):

They used to be red. I'm not going crazy, right?

Bryan Gin-ge Chen (Oct 26 2021 at 20:44):

Aha: https://github.blog/changelog/2021-10-26-updates-to-our-issue-status-icons-and-colors/

Arthur Paulino (Oct 26 2021 at 20:47):

Interesting. Purple is the same color of the "merged" icons on PRs. Makes sense to me.

Eric Wieser (Oct 26 2021 at 20:48):

Here is a purple checkmark on a non-bors'd closed PR: https://github.com/leanprover-community/mathlib/pull/3475

Last updated: Dec 20 2023 at 11:08 UTC