Hi @philcerf.
Thank you @Jelle for reviewing the PR.
Philippe, thank you for the PR, your patience with it, and for bringing it to our attention.
As an FYI to others who may be reading this post, the devguide mentions reviews and asking for someone to take a look at an open PR: Lifecycle of a pull request