>A slight whoopsy in trying to `git push origin a034d7e5...:master'. I >tried a --dry-run with `master:a034d7e5...' and it didn't complain so >did it for real. Unfortunately, it appears to have created a new branch >called, yep, `a034d7e5...'. And well as polluting the public repo, it >makes local git unhappy because a 40-long hex-string is ambiguous. How >does that get fixed?
I believe it is relatively simple to delete a remote branch once it has been merged (it's one of those things I'll need to look up, but I recall doing it before). Do you want me to do that, or would you rather fix it? --Ken -- Nmh-workers https://lists.nongnu.org/mailman/listinfo/nmh-workers
