Closed jimblandy closed 4 years ago
Nothing too surprising, I hope.
Hm... I hit merge, and github shows the commits merged, but this PR now says it has conflicts instead of that it was merged...
Going to just close this, I guess.
Nothing too surprising, I hope.