For git push
there are a lot of defaults. Let's start with clearly separating out the various pieces of syntax. The syntax, abbreviated a bit further to the parts of interest, goes like this:
git push [options] [repository [refspec ...]]
The repository
argument is typically the name of a remote, such as origin
, but could be a URL. If no repository
argument is specified on the command line, no refspec
can be specified either: the options are prefixed by dashes, and whatever's not dash-prefixed, the first word (as split into argv
elements by whatever invokes C-compiled programs on the system in question) is the repository, and additional words are the refspecs. However, it is definitely possible to give a repository without giving a refspec. For instance, git push
lacks both, while git push origin
has a repository but lacks a refspec.
The case we are interested in here is when the refspec isn't on the command line. However, it works the same as when the refspec is on the command line—it's just that the places Git looks, in order to find some refspec or refspecs, can be set in the configuration.
Let's say that the repository specified on the command line was origin
, i.e., you ran git push origin
. Git will, as you said, check your configuration to see if you have a remote.origin.push
setting. Let's say further that, initially:
git config --get remote.origin.push
prints the string develop:benjamin_develop
.
This is a refspec that has both <src>
and :<dst>
parts, so Git treats it as develop:benjamin_develop
.
Now let's say you run:
git config remote.origin.push develop
i.e., take away the :benjamin_develop
part of the setting. You then run git push origin
again. Now the implied refspec is just develop
: it is missing its :<dst>
part.
The paragraph you quoted is pretty confusing (it confused me), but after experimentation—see comments below—we found that it acts the same as:
git push origin develop
on the command line, which acts the same as:
git push origin develop:develop
i.e., the :<dst>
part is just the same as the :<src>
part, regardless of the current push.default
setting.
(I think the documentation here could be clearer. The fundamental problem is that Git's behavior has grown and changed a lot over time. The remote.<remote>.push
setting did not exist in older versions of Git, so at some point, when it was added, someone had to add a paragraph to the documentation to match. At this point, the documentation as a whole could be refactored to eliminate redundancy, but no one has done that.)