[HEADS UP] The master branch has been force pushed

[Andrea Cosentino]

Hello,

If you see the local master branch diverged from origin master, please do a
git pull --rebase.

Please, the next time, avoid force pushing on any branch.

Force pushing should be used in a just a few cases.

Thanks.