[tor-commits] [tor/master] scripts/git: Make the git push command and args configurable