I do not think having "git push" as example is a good idea.
The command has a very high chance of pushing things which are unwanted to be
pushed
Reviewed-by: Carl Eugen Hoyos <cehoyos@ag.or.at>
Signed-off-by: Michael Niedermayer <michael@niedermayer.cc>