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