Oops, I meant to post, for posterity, that I submitted this as a PR a couple of weeks ago … I’m not familiar with how long PRs take to get accepted or rejected, on average, so I guess it’s just a wait-and-see.
Oops, I meant to post, for posterity, that I submitted this as a PR a couple of weeks ago … I’m not familiar with how long PRs take to get accepted or rejected, on average, so I guess it’s just a wait-and-see.