remote/git-push

   1 #!/bin/sh -eu
   2 tool=$(readlink -e "${0%/*}/..")
   3 . "$tool"/remote/lib.sh
   4
   5 remote=${1:-$local_fqdn}; shift
   6 GIT_SSH="$tool"/remote/ssh git push -v "$remote" "$@"