Archived – this site ended its life on 2022.01.02. For the next microblogging site from Chris Krycho, see v1.microblog.chriskrycho.com.

Quick Git tip: if you’ve manually edited your Git configuration file and removed a given remote, you may find yourself in a spot where you now have a bunch of branches associated with that remote… which you cannot delete. The only way (I could find) out of this problem was to re-add the remote, and then run git remote rm <the name of the remote>. That deleted the remote and all the references to its branches