Actually I'm a bit unsure what the problem is now, since there were no intervening commits ? My suggestion was simply that merging the second of my original PRs after inadvertently merging the first should be equivalent to, and less noisy in the git history than reverting one and then merging the PR that combined them. Now we're looking at revert&revert-the-revert which is bound to be even more noisy ?

Actually I'm a bit unsure what the problem is now, since there were no intervening commits ? My suggestion was simply that merging the second of my original PRs after inadvertently merging the first should be equivalent to, and less noisy in the git history than reverting one and then merging the PR that combined them. Now we're looking at revert&revert-the-revert which is bound to be even more noisy ?

Github didn't let us merge your PR #1057 after we accepted #1046. I suspect it is because they shared same commit hashes, if that is really the case. Reverting the merge didn't help.