On 14/04/2021 14:28, Mark Wielaard wrote:
I added the following line to my .git/config at the end of the [remote
"origin"] section to be able to pull it:
fetch = +refs/pull/*/head:refs/remotes/origin/pr/*
Then git pulled and checkout pr/4, made the changes, committed them
and pushed them back, hoping that would update the pr.
Is there anywhere that works?
I don't think even github allows you to push back to the
generated head for the PR like that. If the person who opened
the PR allowed it then you can push to their original branch
to update the PR - no idea if pagure supports that.
Possibly src.fpo should reject pushes to the PR heads to
avoid this kind of accident though.
But it didn't, apparently I created a new origin/pr/4 branch, which I
am now unable to delete because:
$ git push origin --delete pr/4
remote: Branch deletion is not allowed
remote: Denied push for ref 'refs/heads/pr/4' for user 'mjw'
remote: All changes have been rejected
To ssh://pkgs.fedoraproject.org/rpms/valgrind
! [remote rejected] pr/4 (pre-receive hook declined)
error: failed to push some refs to 'ssh://pkgs.fedoraproject.org/rpms/valgrind'
What did I do wrong and how do I fix this?
You pushed a branch into source git which is bad as hey
can't be deleted.
I believe in principle you can ask an admin to delete it
so long as no builds have been done from it.
Tom
--
Tom Hughes (t...@compton.nu)
http://compton.nu/
_______________________________________________
devel mailing list -- devel@lists.fedoraproject.org
To unsubscribe send an email to devel-le...@lists.fedoraproject.org
Fedora Code of Conduct:
https://docs.fedoraproject.org/en-US/project/code-of-conduct/
List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines
List Archives:
https://lists.fedoraproject.org/archives/list/devel@lists.fedoraproject.org
Do not reply to spam on the list, report it:
https://pagure.io/fedora-infrastructure
