Johannes Sixt [off-list ref] wrote:
$ git gc --auto --quiet
Auto packing your repository for optimum performance. You may also
run "git gc" manually. See "git help gc" for more information.
[...]
[*] Skipping the hint to "run git gc manually" would even be good in
this case, because the hint pertains the remote repository, not the
one from which "git push" was issued.
I agree with your suggestions. On the same note, while we're already
changing the message, it might make sense to change it to "Auto packing
the repository [...]".
Jan