Especially when using Github branch and push workflows repos can
easily have hundreds of branches. The role mirror-workspace-git-repos
which pushes them onto the node prints all of them in every
build. This can get quite messy. Thus we need to optionally be able to
silence the git push operation. This is done on purpose by the --quiet
parameter instead of using no_log because this way errors are still
logged normally and normal operation produces no log output for this
task.
Change-Id: Id77cc00972df9139e4544dd79954d91f4ab6b60b
4ea777ae66