diff options
author | Felipe Contreras <felipe.contreras@gmail.com> | 2012-02-23 00:43:41 +0200 |
---|---|---|
committer | Junio C Hamano <gitster@pobox.com> | 2012-02-22 18:17:39 -0800 |
commit | 6ddba5e241ebe484d53e3573c72386f487e25697 (patch) | |
tree | 836c5b5f1ee5d900e87ea9d60c32e576e219b68f /builtin/push.c | |
parent | 676552464a871564835e1cb9d0484277b1b75e79 (diff) | |
download | git-6ddba5e241ebe484d53e3573c72386f487e25697.tar.gz |
push: add '--prune' optionfc/push-prune
When pushing groups of refs to a remote, there is no simple way to remove
old refs that still exist at the remote that is no longer updated from us.
This will allow us to remove such refs from the remote.
With this change, running this command
$ git push --prune remote refs/heads/*:refs/remotes/laptop/*
removes refs/remotes/laptop/foo from the remote if we do not have branch
"foo" locally anymore.
Signed-off-by: Felipe Contreras <felipe.contreras@gmail.com>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
Diffstat (limited to 'builtin/push.c')
-rw-r--r-- | builtin/push.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/builtin/push.c b/builtin/push.c index 35cce532f2..fdfb2c4512 100644 --- a/builtin/push.c +++ b/builtin/push.c @@ -261,6 +261,8 @@ int cmd_push(int argc, const char **argv, const char *prefix) OPT_BIT('u', "set-upstream", &flags, "set upstream for git pull/status", TRANSPORT_PUSH_SET_UPSTREAM), OPT_BOOLEAN(0, "progress", &progress, "force progress reporting"), + OPT_BIT(0, "prune", &flags, "prune locally removed refs", + TRANSPORT_PUSH_PRUNE), OPT_END() }; |