Learn more about these different git repos.
Other Git URLs
Sometimes when a PR is merged, PR says its closed and merged but its not actually getting merged into main repo.
The problem here is, its not consistent and I think its a race condition between two merges or something.
One example is https://pagure.io/pungi-fedora/pull-request/170 but its got pushed to main repo manually.
Just saw this with https://pagure.io/fedora-kickstarts/pull-request/170. @ausil had to manually push the changes into the repo.
This is a pretty major bug IMHO.
other related bug: https://pagure.io/pagure/issue/1190
this is a dupe of #1190
One common denominator I'm seeing on all this PRs is that they are not targeting the main branch, I'll try to replicate this locally and see if I can find something.
FTR, I tried replicating it locally w/ no luck :(
Another example: https://pagure.io/fedora-kickstarts/pull-request/181
Commit a5677e9 fixes this issue
Login to comment on this ticket.