Mention git-revert as an alternative to git-reset to revert changes.
Signed-off-by: Robin Rosenberg <robin.rosenberg@dewire.com>
Signed-off-by: Junio C Hamano <junkio@cox.net>
commits, they will be lost. Also, don't use "git reset" on a
publicly-visible branch that other developers pull from, as it will
force needless merges on other developers to clean up the history.
+If you need to undo changes that you have pushed, use gitlink:git-revert[1]
+instead.
The git grep command can search for strings in any version of your
project, so