Hi Ken,
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...'.
I should have done, and later did, `a034d7e5:master'; the other way
around.
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?
I'm happy to have a go. Will wait a bit and do some research.
Hopefully it won't compound the error. :-)
--
Cheers, Ralph.
https://plus.google.com/+RalphCorderoy
--
Nmh-workers
https://lists.nongnu.org/mailman/listinfo/nmh-workers