Re: [HEADS UP] The master branch has been force pushed

[Jean-Baptiste Onofre]

Hi,

Agree with Andrea. By the way, we can "block" force push on gitbox (it’s what I 
did on Karaf to avoid any mistake).

Regards
JB

> Le 19 mai 2020 à 08:17, Andrea Cosentino <anco...@gmail.com> a écrit :
> 
> 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.