From the linked PR, it is unclear to me if the change was already merged upstream. I dropped a comment in the closed PR.
From the linked PR, it is unclear to me if the change was already merged upstream. I dropped a comment in the closed PR.