Closed fredrik-johansson closed 1 month ago
What's up with the CI? Have we hit some limit?
Seems to only affect the runners with Ubuntu 24.04 running more than 4 minutes.
BTW, why do we run duplicate tests (both (push) and (pull_request)) on PRs? I thought at some point this was fixed so only one was run.
I wrote about the issue of Ubuntu 24.04 runners here: https://github.com/actions/runner-images/issues/9848#issuecomment-2137140734
BTW, why do we run duplicate tests (both (push) and (pull_request)) on PRs? I thought at some point this was fixed so only one was run.
Because you are pushing to flintlib
user/organization's repository of FLINT. I don't know how to fix this. Perhaps Doctor @edgarcosta knows how?
True, I should maybe just go back to using my own repo :-)
BTW, why do we run duplicate tests (both (push) and (pull_request)) on PRs? I thought at some point this was fixed so only one was run.
Because you are pushing to
flintlib
user/organization's repository of FLINT. I don't know how to fix this. Perhaps Doctor @edgarcosta knows how?
That is exactly what @albinahlback said. For organizational purposes, we should always work on our personal forks, make PRs to main, and perhaps protect main from accidental pushes. https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/managing-protected-branches/about-protected-branches
Alternatively, we could add something to prevent the double CI run, e.g.: (this is not tested)
if: (github.event_name != 'pull_request' && ! github.event.pull_request.head.repo.fork) || (github.event_name == 'pull_request' && github.event.pull_request.head.repo.fork))
Current profile vs acf: