man git-pull sayeth
In its default mode, git pull is shorthand for git fetch followed by
git merge FETCH_HEAD.
However, I just tried that and it failed rather spectacularly. How do
you *really* update your local repo without an extra git fetch step?
Poking around, it looks like each workdir has its own copy of
.git/FETCH_HEAD, which may be the problem --- I was trying to update a
workdir that wasn't the one I'd done git fetch in. Do I have to put
together a script that copies FETCH_HEAD from place to place?
regards, tom lane