This is a copy of this pull request; after fixing the addition of an accidental merge commit.
I've planned to overwrite the branch used here, but I must have made a mistake pushing or using git --set-upstream-to. So, instead, my original branch got deleted.
This is a copy of this pull request; after fixing the addition of an accidental merge commit.
I've planned to overwrite the branch used here, but I must have made a mistake pushing or using
git --set-upstream-to. So, instead, my original branch got deleted.