On 24.07.2019 20:05, Ben Pfaff wrote: > Signed-off-by: Ben Pfaff <[email protected]> > --- > Based on an off-lst discussion with Ilya. This is just my first, off-hand > thought on the topic. Feedback welcome!
We could also consider suggesting a git hook like that: --- $ cat .git/hooks/pre-push #!/bin/bash remote=$1 protected_remote='upstream' if [ $protected_remote != $remote ]; then exit 0; fi echo "You're about to push to $protected_remote." read -p "Do you want to proceed? [y|n] " reply < /dev/tty if echo $reply | grep -E '^[Yy]$' > /dev/null; then exit 0; fi exit 1 --- > > diff --git a/Documentation/internals/committer-responsibilities.rst > b/Documentation/internals/committer-responsibilities.rst > index 4d10c3980875..b34dddaa99fd 100644 > --- a/Documentation/internals/committer-responsibilities.rst > +++ b/Documentation/internals/committer-responsibilities.rst > @@ -94,3 +94,9 @@ Use Reported-by: and Tested-by: tags in commit messages to > indicate the > source of a bug report. > > Keep the ``AUTHORS.rst`` file up to date. > + > +If you mistakenly push a commit that should not have been applied, it's OK to > +use a Git "force-push" to remove it from the tree, as long as you do it > within > +a few minutes and no one has pushed other commits to the tree in the > meantime. > +Otherwise, it's necessary to revert the commit. (If you do this frequently, > +more than once or twice a year, then maybe you should be more careful.) > _______________________________________________ dev mailing list [email protected] https://mail.openvswitch.org/mailman/listinfo/ovs-dev
