For Git push messages, we now have a single space character between
the name of a commit's author and the number of commits by that
author, plus a period at the end.
Part of #3968.
Follow-up to #4006.
We now use the name of the author of a commit as opposed to the
committer to format Git messages with multiple committers.
Part of #3968.
Follow-up to #4006.
We now show a few new things:
(1) The number of commits pushed.
(2) Who authored the commits (just counts, not which specific ones, for brevity).
Add tests for case of multiple committers.
Part of #3968.