Re: [PATCH 5/8] push, send-pack: support pushing HEAD to real ref name

Junio C Hamano [off-list ref] writes:

Steffen Prohaska [off-list ref] writes:

quoted

On Oct 28, 2007, at 8:28 AM, Junio C Hamano wrote:

quoted

Steffen Prohaska [off-list ref] writes:

quoted

This teaches "push <remote> HEAD" to resolve HEAD on the local
side to its real ref name, e.g. refs/heads/master, and then
use the real ref name on the remote side to search a matching
remote ref.

This probably is a good idea.

I'll add an even shorter shorthand: "git push HEAD" will push
the current branch to its default remote.

Ugh, that looks way too magicky.  The first parameter to push if
one ever exists has _always_ been the remote, and the above
breaks it.

Please don't.

An alternative, just to let me keep my nicer public image by
pretending to be constructive ;-)

Introduce a configuration "remote.$name.push_default" whose
value can be a list of refs.  Teach the push command without
refspecs:

	$ git push
	$ git push $remote

to pretend as if the listed refspecs are given, instead of the
traditional "matching branches" behaviour.

Then, introduce another option

	$ git push --matching
	$ git push --matching $remote

to override that configuration, if set, so that the user who
usually pushes only the selected branches can use the "matching
branches" behaviour when needed.

Along with your earlier "git push $remote HEAD" patch, this will
allow you to say:

	[remote "origin"]
        	push_default = HEAD

and your

	$ git push

will push only the current branch.

On Oct 28, 2007, at 5:03 PM, Junio C Hamano wrote:

Junio C Hamano [off-list ref] writes:

quoted

Steffen Prohaska [off-list ref] writes:

quoted

On Oct 28, 2007, at 8:28 AM, Junio C Hamano wrote:

quoted

Steffen Prohaska [off-list ref] writes:

quoted

This teaches "push <remote> HEAD" to resolve HEAD on the local
side to its real ref name, e.g. refs/heads/master, and then
use the real ref name on the remote side to search a matching
remote ref.

This probably is a good idea.

I'll add an even shorter shorthand: "git push HEAD" will push
the current branch to its default remote.

Ugh, that looks way too magicky.  The first parameter to push if
one ever exists has _always_ been the remote, and the above
breaks it.

Please don't.

An alternative, just to let me keep my nicer public image by
pretending to be constructive ;-)

Introduce a configuration "remote.$name.push_default" whose
value can be a list of refs.  Teach the push command without
refspecs:

	$ git push
	$ git push $remote

to pretend as if the listed refspecs are given, instead of the
traditional "matching branches" behaviour.

Then, introduce another option

	$ git push --matching
	$ git push --matching $remote

to override that configuration, if set, so that the user who
usually pushes only the selected branches can use the "matching
branches" behaviour when needed.

Along with your earlier "git push $remote HEAD" patch, this will
allow you to say:

	[remote "origin"]
        	push_default = HEAD

and your

	$ git push

will push only the current branch.

Sounds reasonable; but it is more work. I'm not starting to
implement this today.

	Steffen