You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I opened the PR using the web editor, and thus the branch got named lgoettgens-patch-1.
However, the CI jobs created by OscarDevTools have different names than they have in all other cases.
I agree with the idea behind this that we should never try to match these kinds of branches to the ones in other downstream repositories, but that shouldn't be the reason for this discrepancy.
expected job name: matching: [Nemo#master,Hecke#master] - ubuntu-latest, julia ~1.10.0-0
real job name: [Nemo,Hecke]#master - ubuntu-latest, julia ~1.10.0-0
Due to this difference, one always needs to circumvent branch protection rules to merge these kinds of PRs.
The text was updated successfully, but these errors were encountered:
See e.g. Nemocas/AbstractAlgebra.jl#1811.
I opened the PR using the web editor, and thus the branch got named
lgoettgens-patch-1.However, the CI jobs created by OscarDevTools have different names than they have in all other cases.
I agree with the idea behind this that we should never try to match these kinds of branches to the ones in other downstream repositories, but that shouldn't be the reason for this discrepancy.
expected job name:
matching: [Nemo#master,Hecke#master] - ubuntu-latest, julia ~1.10.0-0real job name:
[Nemo,Hecke]#master - ubuntu-latest, julia ~1.10.0-0Due to this difference, one always needs to circumvent branch protection rules to merge these kinds of PRs.
The text was updated successfully, but these errors were encountered: