Push options are a capability in the Git protocol to transport
arbitrary strings (example usage: topic strings) to the server through
command line flags rather than by the existing Gerrit-specific magic
branch "refs/for/master%..." convention.
For example with Git >= 2.10:
git push -o r=email -o topic=fix-bug42 origin HEAD:refs/for/master
can now be used instead of:
git push origin HEAD:refs/for/master%r=email,topic=fix-bug42
Change-Id: I44e7214b9342d461b07c4b6dd638970cf5fb622f
Signed-off-by: Dan Wang <dwwang@google.com>