git-push.txt: document the behavior of --repo