Re: [PATCH 2/2] push: add '-d' as shorthand for '--delete'

[Jeff King <peff@peff.net>]

On Wed, Dec 16, 2015 at 12:29:38PM -0800, Junio C Hamano wrote:

> Jeff King <peff@peff.net> writes:
> 
> > At this point, it seems that "--delete" is useful, and nothing else has
> > been proposed for "-d" in the intervening years. It seems like a
> > reasonable use of the flag to me.
> 
> I think there were two (and a half) reasons why we didn't let
> "--delete" use a short-and-sweet "-d", and I agree that "something
> else that is more useful did not come" removes one of them.
> 
> The other reason was to avoid the chance of fat-fingering, because
> deleting is destructive, and it is even harder to recover from if
> the damage is done remotely (and the remaining one-half is that
> deleting is a rare event).
> 
> Even though I do not think the need for the "safety" has been
> reduced over time to warrant this change, a similarity with "branch"
> that has "-d/--delete" would be a good enough argument to support
> this change.

Thanks for the input, I hadn't considered "safety" at all. We do have
safety measures on "git branch -d" that we don't have here. I guess we
could implement something similar (e.g., see if the to-be-deleted branch
is merged elsewhere; of course we might not have the objects locally at
all). On the other hand, you can already screw yourself pretty badly
with "push -f".

So I think it's probably OK to add "-d".

-Peff