make update should do git pull

[poussa]

I was expecting make update to do

• git clone repo if it does not exists, or git pull to update to the HEAD from the origin
• git check out the commit listed in deps/repos.txt

The git pull part missing. I ended up having an old git tree which did not have the commit id listed in repos.txt. So the tree is stuck with the cloned version.

Can we fix this?

[jprestwo]

#142

I was thinking about this and, though I don't see anything wrong with it, it should not make a difference unless we have a specific branch/master in repos.txt. A commit ID shouldn't matter if you do a git pull after checkout (right?). Either way it couldn't hurt.

[poussa]

This has been already fixed.