Git: modificare l'URL di un repository remoto

In questi giorni mi è successa una cosa abbastanza strana (per me, almeno): ho iniziato a sviluppare un'applicazione, poi effettivamente ho scoperto che il nome che le avevo dato non solo era già preso da un'altra app (che mi aveva pure fregato il dominio), ma era registrato come trademark eccetera eccetera, cosicché se l'avessi usato comunque avrei fatto un grave torto al suo utilizzatore primario. Insomma, ho deciso di cambiare nome all'applicazione.

Posto che non voglio discutere se sia giusto o meno assegnare un nome "ufficiale" a dei repository per app ancora in sviluppo, ho cambiato quindi anche nome al repository Git dove facevo push dei miei cambiamenti: essendo lo sviluppo portato avanti su più macchine, ho avuto delle difficoltà di tipo "rottura di cosiddetti" a migrare al nuovo repository, almeno finché non ho deciso di aprire il manuale di Git per controllare se "origin" potesse essere modificato senza particolari rogne. Così, ho studiato un po'.

Per modificare un URL di un qualsiasi repository remoto a cui abbiamo assegnato uno short name, ci basta dare questo comando da terminale:

git config remote.origin.url $URL

Il che ovviamente corrisponde al modificare il repository origin. Se il repository si chiama pippo, ovviamente ci basterà modificare il nome del repository, intuitivamente:

git config remote.pippo.url $URL

Fine della storia. Così possiamo cambiare URL del repository remoto ogni volta che vogliamo. Ovviamente, per team di grandi dimensioni, è necessario avvisare all'interno del flusso di lavoro di stare fermi, pena trovarsi con commit e push mandati a carte quarantotto, specie se chi lavora al progetto fa parecchie push. Ah, la bellezza della continous integration.

Poscritto - Fulvio mi ha appena ricordato su Facebook che c'è anche un altro modo; da Git 1.7 possiamo anche dare il seguente comando:

git remote set-url origin $URL