Note that I'm merging these kinds of PRs quickly because I don't think there's any debate about whether or not we want the change. I someone wants to review, you're welcome to do so even after it is merged! Things can always be changed or even reverted.
Note that I'm merging these kinds of PRs quickly because I don't think there's any debate about whether or not we want the change. I someone wants to review, you're welcome to do so even after it is merged! Things can always be changed or even reverted.