git push usage

The man page for git push claims:

 --repo=<repository>
     This option is only relevant if no <repository> argument is passed
     in the invocation. In this case, git-push derives the remote name
     from the current branch: If it tracks a remote branch, then that
     remote repository is pushed to. Otherwise, the name "origin" is
     used. For this latter case, this option can be used to override the
     name "origin". In other words, the difference between these two
     commands

         git push public         #1
         git push --repo=public  #2

     is that #1 always pushes to "public" whereas #2 pushes to "public"
     only if the current branch does not track a remote branch. This is
     useful if you write an alias or script around git-push.

However, I'm sitting here looking at the code and I don't see how this is possible. I've also done some testing. So I think the man page lies and that forms (1) and (2) are equivalent as shown.

cmd_push() is:

  const char *repo = NULL; /* default repository */
  struct option options[] = {
    ...
    OPT_STRING( 0 , "repo", &repo, "repository", "repository"),
    ...
  }

  argc = parse_options(argc, argv, options, push_usage, 0);

  if (argc > 0) {
    repo = argv[0];
    set_refspecs(argv + 1, argc - 1);
  }

  rc = do_push(repo, flags);

So if the user specifies --repo, then its value is assigned to *repo by parse_options. If the user otherwise specifies a repository w/o --repo, that will be argv[0] after parse_options, so it will get assigned to *repo. Assuming no other arguments, set_refspecs gets called with argc = 0 and returns w/o doing anything.

So the only difference I can see is that form #1 allows the user to specify a refspec on the command line. Form #2 does not since the first non-dashed argument gets assigned to *repo, so:

$ git push --repo src:dst

would assign src:dst to *repo, which would choke.

So, what's the point of the --repo dashed-option then?

j.