As per the code, the --repo <repo> option is equivalent to the
<repo> argument to 'git push', but somehow it was documented as
something that is more than that. [It exists for historical
reasons, back from the time when options had to come before
arguments.]
Say so. [But not that.]
Signed-off-by: Michael J Gruber <git@drmicha.warpmail.net> Helped-by: Eric Sunshine <sunshine@sunshineco.com> Signed-off-by: Junio C Hamano <gitster@pobox.com>