git-branch: display "was sha1" on branch deletion rather than just "sha1"

diff --git a/Documentation/git-push.txt b/Documentation/git-push.txt
index c44dce374a39566c2ad349c657e582c6a8a8d8ec..6150b1b959e17655a2875d39ec3b70449684a0eb 100644 (file)
--- a/Documentation/git-push.txt
+++ b/Documentation/git-push.txt
@@ -9,8 +9,9 @@ git-push - Update remote refs along with associated objects
 SYNOPSIS
 --------
 [verse]
-'git push' [--all] [--dry-run] [--tags] [--receive-pack=<git-receive-pack>]
-           [--repo=all] [-f | --force] [-v | --verbose] [<repository> <refspec>...]
+'git push' [--all | --mirror] [--dry-run] [--tags] [--receive-pack=<git-receive-pack>]
+          [--repo=<repository>] [-f | --force] [-v | --verbose]
+          [<repository> <refspec>...]
 
 DESCRIPTION
 -----------
@@ -29,9 +30,9 @@ OPTIONS
        The "remote" repository that is destination of a push
        operation.  See the section <<URLS,GIT URLS>> below.
 
-<refspec>::
+<refspec>...::
        The canonical format of a <refspec> parameter is
-       `+?<src>:<dst>`; that is, an optional plus `+`, followed
+       `+?<src>:<dst>`; that is, an optional plus `{plus}`, followed
        by the source ref, followed by a colon `:`, followed by
        the destination ref.
 +
@@ -100,9 +101,23 @@ nor in any Push line of the corresponding remotes file---see below).
        This flag disables the check.  This can cause the
        remote repository to lose commits; use it with care.
 
---repo=<repo>::
-       When no repository is specified the command defaults to
-       "origin"; this overrides it.
+--repo=<repository>::
+       This option is only relevant if no <repository> argument is
+       passed in the invocation. In this case, 'git-push' derives the
+       remote name from the current branch: If it tracks a remote
+       branch, then that remote repository is pushed to. Otherwise,
+       the name "origin" is used. For this latter case, this option
+       can be used to override the name "origin". In other words,
+       the difference between these two commands
++
+--------------------------
+git push public         #1
+git push --repo=public  #2
+--------------------------
++
+is that #1 always pushes to "public" whereas #2 pushes to "public"
+only if the current branch does not track a remote branch. This is
+useful if you write an alias or script around 'git-push'.
 
 --thin::
 --no-thin::
@@ -180,11 +195,11 @@ git push origin :experimental::
        Find a ref that matches `experimental` in the `origin` repository
        (e.g. `refs/heads/experimental`), and delete it.
 
-git push origin master:satellite/master::
-       Find a ref that matches `master` in the source repository
-       (most likely, it would find `refs/heads/master`), and update
-       the ref that matches `satellite/master` (most likely, it would
-       be `refs/remotes/satellite/master`) in `origin` repository with it.
+git push origin master:satellite/master dev:satellite/dev::
+       Use the source ref that matches `master` (e.g. `refs/heads/master`)
+       to update the ref that matches `satellite/master` (most probably
+       `refs/remotes/satellite/master`) in the `origin` repository, then
+       do the same for `dev` and `satellite/dev`.
 
 git push origin master:refs/heads/experimental::
        Create the branch `experimental` in the `origin` repository
@@ -195,7 +210,7 @@ git push origin master:refs/heads/experimental::
 
 Author
 ------
-Written by Junio C Hamano <junkio@cox.net>, later rewritten in C
+Written by Junio C Hamano <gitster@pobox.com>, later rewritten in C
 by Linus Torvalds <torvalds@osdl.org>
 
 Documentation