Merge branch 'mm/push-simple-doc' into maint

The documentation did not clearly state that the 'simple' mode is
now the default for "git push" when push.default configuration is
not set.

* mm/push-simple-doc:
  Documentation/git-push: document that 'simple' is the default

Author: gitster

Documentation/git-push.txt

@@ -37,6 +37,13 @@ the default `<refspec>` by consulting `remote.*.push` configuration,
 and if it is not found, honors `push.default` configuration to decide
 what to push (See linkgit:git-config[1] for the meaning of `push.default`).
 
+When neither the command-line nor the configuration specify what to
+push, the default behavior is used, which corresponds to the `simple`
+value for `push.default`: the current branch is pushed to the
+corresponding upstream branch, but as a safety measure, the push is
+aborted if the upstream branch does not have the same name as the
+local one.
+
 
 OPTIONS[[OPTIONS]]
 ------------------