Ah, sorry about that. I made #141 through the VSCode extension Github Pull Requests. Sometimes it'll select the a base branch different from the default branch. There's probably a reason, but I haven't discovered it yet, as it happens rarely. Then I don't pay attention to it, since it normally selects the correct base branch, and I create the PR with the wrong base branch. And for the same reason on Github nobody expects the base branch of a PR to be wrong. So it gets merged into the wrong branch. I've had it a couple of times over the past few years.