On 14/01/2020 13:37, Jonathan Wakely wrote: > I really think people should be reviewing what they're about to push > before doing it. > > OK for wwwdocs? >
I'd recommend git push origin HEAD:<target-branch> rather than just 'git push' Otherwise, OK. R.