Zulip Chat Archive

Stream: general

Topic: CI troubles

Yaël Dillies (Mar 22 2022 at 17:08):

It seems we're experiencing troubles with #CI at the moment. Lint style is skipped.

Ruben Van de Velde (Mar 22 2022 at 17:10):

I think GitHub is having troubles again

Bryan Gin-ge Chen (Mar 22 2022 at 17:10):

Yep, some kind of incident is in progress: https://www.githubstatus.com/

Gabriel Ebner (Mar 22 2022 at 17:12):

Bors seems to be down as well: https://app.bors.tech/

Yaël Dillies (Mar 22 2022 at 17:14):

Precisely when I was going to get 10 merged PR in a day :sob:

Yaël Dillies (Mar 22 2022 at 18:58):

#12286 and #12879 haven't been picked up by #bors.

Yaël Dillies (Mar 22 2022 at 19:36):

...and #11282

Mauricio Collares (Mar 22 2022 at 19:47):

For the delegated ones, can you type bors merge again?

Yaël Dillies (Mar 22 2022 at 19:52):

#12879, yes. #11282, no, because bors didn't pick up the delegation.

Bryan Gin-ge Chen (Mar 22 2022 at 19:59):

Thanks! I've put #12286 and #11282 on the queue (and also delegated just in case).

Aaron Anderson (Mar 22 2022 at 20:02):

Can we get #12837 back on the queue also?

Bryan Gin-ge Chen (Mar 22 2022 at 20:03):

Done!

Yaël Dillies (Mar 23 2022 at 21:49):

And #12876, @Bryan Gin-ge Chen

Last updated: Dec 20 2023 at 11:08 UTC