On Wed, Apr 14, 2021 at 02:38:40PM +0100, Tom Hughes via devel wrote:
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.
I have no experience with github, but it looked like a normal remote
branch to me, so I expected to be able to push to it. How else are you
supposed to coordinate on a PR/patch like that?
Possibly src.fpo should reject pushes to the PR heads to
avoid this kind of accident though.
Yes, I did certainly mess up here, don't completely understand how,
but it would have been nice if the system would have stopped me.
> 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.
That would be nice. How do I contact an admin?
Thanks,
Mark