Git voit double

Hello les gens !

Une petite prise de notes rapide, parce que je sais que je vais tout oublier si je ne le fais pas :)

Il m’arrive souvent, depuis que je streame, d’avoir besoin de deux remotes sur mes dépots git : un remote public, typiquement github ou gitlab, et un remote privé. Le problème de cette approche est que je dois taper deux fois “git push” : un vers chacun de mes remotes. C’est une perte de temps, un risque d’oubli … Bref, pas satisfait le Rancune !

Il s’avère qu’il existe une autre solution : donner deux adresses de push au même remote. C’est pas très compliqué, il suffit de faire :

git remote set-url --add --push origin <adresse du repo 1>
git remote set-url --add --push origin <adresse du repo 2>

Et hop ! Le remote “origin” a désormais deux adresses de push. Par exemple, pour un de mes projets, cela donne :

+ git remote -v
origin  seb@coffee:./git/devel_hw/GenericLib.git (fetch)
origin  git@github.com:Rancunefr/GenericLib.git (push)
origin  seb@coffee:./git/devel_hw/GenericLib.git (push)

Lorsque l’on fait un push, il sera désormais automatiquement effectué deux fois.

Rancune.