Closed giordano closed 3 months ago
Instead of deleting it wholesale, shall we just comment out the relevant line in the "launch unsigned jobs" section? This makes it much easier to undo this change in the (unlikely) event that we decide to switch this job back to Buildkite in the future.
I have merged https://github.com/JuliaLang/julia/pull/55281
I think an admin needs to remove this job from the required ones for a merge.
I think an admin needs to remove this job from the required ones for a merge.
Done.
Close-reopen doesn't usually do anything to Buildkite.
I know, but it does for the required jobs status, which is now reset and the PR can be merged.
This is now running in GitHub Actions. Companion PR to https://github.com/JuliaLang/julia/pull/55281, it should be merged only after that one is merged.