On Sun, Feb 16, 2020 at 6:56 PM David Kastrup <[email protected]> wrote: > >> Han-Wen Nienhuys <[email protected]> writes: > >> > >> > sorry, my mistake (another reason to move to different tooling.) > >> > >> I very strongly disagree. We don't want to move to a tooling where > >> material that is untested in its context gets pushed to the resource > >> > > > > You don't understand what I'm trying to say. > > > > If there is a policy that nobody pushes directly to master, the normal > > course of action is to enforce that policy using tooling. Both GitLab > > and GitHub offer "protected branches", see eg. > > https://docs.gitlab.com/ee/user/project/protected_branches.html. Gerrit > > offers per-branch permissions. > > Ok. Strictly speaking that's not as much a matter of the tooling but of > the system administration (part of which is done by tools on > GitLab/GitHub). I have some sketch of a repository hook implementing > our policy (master can only ff, staging _can_ be force-pushed, neither > can be deleted, dev/name is free for name). But installing that would > have meant extra work for the Savannah sysadmins. So in the end I > decided not to bother. The solution would likely have been a better > match to our current workflow than what GitLab can offer, but of course > a partial solution beats an unimplemented solution. > > > It's not that hard to make it a habit to never push to master but > >> instead to staging > > > > > > it's pretty easy to push to master accidentally, because my shell > > history is full of "git push origin HEAD:master" commands. > > I think a push command has enough of an effect that typing it in > manually is not really much of a chore.
II don't believe in manual process. I've installed a hook to prevent this from happening again. https://stackoverflow.com/questions/24695019/git-push-hook-to-disable-push-to-branch Maybe someone can add this to the manual. -- Han-Wen Nienhuys - [email protected] - http://www.xs4all.nl/~hanwen
