rule_git_push () { # SYNTAX: {host|hosted} $git_push_options
local remote=${1#remote=}; shift
GIT_SSH=./vm_ssh git push -v "$remote" "$@"
rule_git_push () { # SYNTAX: {host|hosted} $git_push_options
local remote=${1#remote=}; shift
GIT_SSH=./vm_ssh git push -v "$remote" "$@"