Closed MikeAlhayek closed 4 days ago
I'm wondering why this PR replaces #16962, I already started a PR #16947 before the two but closed as @Piedone suggested to allow the newcomer to start their new PR
I don't see any difference between the PRs except few dots at the end of the comments
Got it, I was just surprised that my PR closed for a reason, then a new PR came in and took time and finally your PR won :)
Thanks for the info
/cc: @AmyBlaine
This PR replaces #16962