Page History

...

Now, you need to re-synch your local clone. It's important to note that committers can do perform some minors minor changes in on your behalf, so always pull the latest changes.
If you were working on a branch, just delete the branch and pull master. You can do this with the following GIT commands.

...

If you were working on master, reset the HEAD back to where origin was and pull master.

REVISIT: Anything better then than the cruel reset --hard?

git reset --hard origin/master

git pull origin master

...