Re: [PATCH 10/10] push: teach push to be quiet if local ref is strict subset of remote ref

Steffen Prohaska [off-list ref] writes:

quoted

You forgot a lot more important part.  Pushing into publishing
repositories.  And the discussion is about git-push command.

Exactly, here are two examples:

If you push only to publishing repositories that are read
only by others, you'll never encounter the problem that
10/10 tried to solve. The publishing repository is never
changed by others. You are the only one who pushes to this
repository. Therefore the remote never advances unexpectedly.

Wrong.

People can and do work from more than one private repositories
(I do).  In a sense, that is sharing the repository with
oneself.

I may do an emergency patch to fix breakage on 'maint' (and
'maint' only) from a location that is not my primary development
box and push the fix out.  I fully expect that the push will
push out 'maint' and expect the other branches such as 'master'
on the remote side to stay the same, as I haven't touched
'master' on that box for quite a while and it is now stale.  In
that situation, I _want_ the "git push" itself to report failure
to notify me that it did not push what _I_ asked it to push out,
so that I can be reminded that I'd better do "git push $remote
maint" the next time.  In the meantime, even though it reports
a failure, 'master' on the remote side is _not_ updated, so the
behaviour is still _safe_.

Another difference is the way changes are integrated. In
a workflow without shared repositories, only pull is used
for integration, while push in only used for publishing the
changes.

Wrong.  push is a mirror of fetch and does not do _any_
integration.  It is just a safe (because it insists on
fast-forward) propagation mechanism.  Your integration still
happens with pull (actually, shared repository people seem to
prefer "fetch + rebase" over "pull" which is "fetch + merge").

This is different if you work with a shared repository. Bob
checks out the shared branch foo to his local branch bar and
later he needs to push bar back to the shared branch foo. Bob
needs to push changes from his local branch bar to the branch
foo in the remote repository, a branch with a different name.
This need does not emerge when working with two publishing
repositories, as described above.

So you do "git push $remote bar:foo".  If you do that regulary,
there are configuration mechanisms to help you reduce your
keyboard wear.  What's the problem?