Originariamente, volevo eliminare un ramo remoto.Differenza tra le potature in git
git push --delete <branchname>
... ha fatto per me. Tuttavia, non ho la differenza tra gli altri comandi:
git push --prune ...
git prune ...
A cosa servono? Il manuale non mi aiuta dal momento che sembra simile e mi sarei aspettato che facessero quello che volevo inizialmente.
git prune agisce sul repository locale, e rimuove oggetti (ad esempio, commette ei file che non sono più raggiungibili da qualsiasi filiale o tag, o da HEAD). git push --prune agisce sul repository remoto, e rimuove rami che non esistono a livello locale (siano davvero attenti con questo comando, in quanto elimina tutti i rami che non hai mai controllato a livello locale, se un ramo è noto al tuo repository locale solo come un ramo remoto, sarà cancellato da remoto).
Ok, grazie - ma il mio ramo locale non esistente che volevo eliminare da remoto (come pure) non è stato cancellato da 'git push --prune' ...? 'git push --delete' lo ha fatto allora. – Xiphias
Lo hai effettivamente eliminato localmente prima? –
Sì, ho usato 'git branch -d' ... dovrebbe aver funzionato allora? Il ramo era sparito quando si guardava 'git branch' –
Xiphias