3 ssh -i vm-key "$to" "$@"
7 source "$target/config"
10 echo "Agent: $SSH_AGENT_PID"
12 if [[ $oldpid == "" ]]; then
16 command=$(basename -- "$0")
17 echo "Action: $command"
18 if [[ $command == "push" ]]; then
19 git push -f "$to:" "HEAD:refs/remotes/manager/master"
21 git fetch "$to:" "+HEAD:refs/remotes/$target/master"
23 if [[ $oldpid == "" ]]; then