Re: `git push --porcelain` has no effect when deleting a ref which does not exist

Xavier Morel <[email protected]> writes:

> Using `push --delete --porcelain` with refs which are extant correctly 
> outputs the relevant information in the documented format:
>
> -	:refs/heads/<branch1>	[deleted]
> -	:refs/heads/<branch2>	[deleted]
>
> However doing the same with refs which don't exist on the remote (e.g. 
> because of a concurrent deletion) has the error written out in 
> human-targeted text:
>
> error: unable to delete '<branch1>': remote ref does not exist
> error: unable to delete '<branch2>': remote ref does not exist
>
> I would have expected something along the lines of:
>
> !	:refs/heads/<branch>	[remote failure]
>
> which would be machine-readable as documented for the `--porcelain` 
> flag. Was that intended or is it just something that fell through the 
> cracks of code convolution?

If I have to guess, I would say it is because nobody thought of
covering this usage pattern, which allows you to randomly throw a
deletion request to probe what does and what does not exist on the
other side.

Patches welcome.

Thanks.