Zulip Chat Archive

Stream: mathlib4

Topic: !4#3884 not on queue4

Kevin Buzzard (May 10 2023 at 19:02):

Should a PR appear on #queue4 the moment it satisfies the requirements? If so then I'm a bit confused about why !4#3884 isn't on there. One of the CI jobs ("Detect changes to header SHAs") failed for some reason, but I re-ran it and it worked. I'm a bit puzzled.

Matthew Ballard (May 10 2023 at 19:12):

GitHub has been having issues today: https://www.githubstatus.com

Kevin Buzzard (May 10 2023 at 20:20):

Thanks! Indeed it's magically there now. In return I reviewed !4#3873 :-)

Last updated: Dec 20 2023 at 11:08 UTC