So git pull is shorthand for what exactly? - Mailing list pgsql-hackers

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