03:21:55 rbrunner7: ping about review on #9939 04:38:50 Oh, looks like GitHub somehow did not inform me. Thanks, will have a go at your comments tomorrow!