Hi! My aim is to delete all those branches in my local git tree that are merged in a specific branch, say, in "develop". I know that I can list those branches by "git branch --merged develop" and that I can delete branches by "git branch -d to_be_deleted". However, I lack experience in bash. So, I used to do the above cleanup using a little Python script that imports sage.dev.all.dev.git.
Since sage.dev.all.dev.git has gone: From where can I import it now? Alternatively, is there a concise way (in bash) to apply "git branch -d" to all branches returned by "git branch --merged develop" that are neither "master" nor "develop"? Best regards, Simon -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To post to this group, send email to sage-devel@googlegroups.com. Visit this group at https://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
