Git : ajouter un second serveur origin pour les push

Une astuce utile si vous travaillez avec un serveur git privé et que vous souhaitez aussi publier votre code sur un serveur public (et inversement) :

# git remote set-url --add --push origin git@gitlab.my.domain:mygroup/project.git