Commit 52f9474d66216e761c681de4459fba21b97eb02b

Thomas de Grivel 2018-01-24T22:15:56

Use git pull instead of fetch and checkout.