user-manual: more explanation of push and pull usage

Recently a user on the mailing list complained that they'd read the
manual but couldn't figure out how to keep a couple private repositories
in sync.  They'd tried using push, and were surprised by the effect.

Add a little text in an attempt to make it clear that:
	- Pushing to a branch that is checked out will have odd results.
	- It's OK to synchronize just using pull if that's simpler.

Signed-off-by: "J. Bruce Fields" <bfields@citi.umich.edu>

diff --git a/Documentation/user-manual.txt b/Documentation/user-manual.txt
index e9da5911f62c01e2ff3ddaf34bfb692c1272ae43..2aed7eb12b4517d8dbc4d86c30b273fa2e92633a 100644 (file)
--- a/Documentation/user-manual.txt
+++ b/Documentation/user-manual.txt
@@ -1772,7 +1772,7 @@ repository, but it works just as well in the other direction.
 
 If you and the maintainer both have accounts on the same machine, then
 you can just pull changes from each other's repositories directly;
-commands that accepts repository URLs as arguments will also accept a
+commands that accept repository URLs as arguments will also accept a
 local directory name:
 
 -------------------------------------------------
@@ -1780,6 +1780,15 @@ $ git clone /path/to/repository
 $ git pull /path/to/other/repository
 -------------------------------------------------
 
+or an ssh url:
+
+-------------------------------------------------
+$ git clone ssh://yourhost/~you/repository
+-------------------------------------------------
+
+For projects with few developers, or for synchronizing a few private
+repositories, this may be all you need.
+
 However, the more common way to do this is to maintain a separate public
 repository (usually on a different host) for others to pull changes
 from.  This is usually more convenient, and allows you to cleanly
@@ -1802,6 +1811,8 @@ like this:
         |               they push             V
   their public repo <------------------- their repo
 
+We explain how to do this in the following sections.
+
 [[setting-up-a-public-repository]]
 Setting up a public repository
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1913,6 +1924,12 @@ proceeding the branch name by a plus sign:
 $ git push ssh://yourserver.com/~you/proj.git +master
 -------------------------------------------------
 
+Note that the target of a "push" is normally a
+<<def_bare_repository,bare>> repository.  You can also push to a
+repository that has a checked-out working tree, but the working tree
+will not be updated by the push.  This may lead to unexpected results if
+the branch you push to is the currently checked-out branch!
+
 As with git-fetch, you may also set up configuration options to
 save typing; so, for example, after