On Mon, 1 May 2023 13:44:22 GMT, Coleen Phillimore <cole...@openjdk.org> wrote:
>> Daniel D. Daugherty has updated the pull request incrementally with one >> additional commit since the last revision: >> >> dholmes CR - change ':' to '.'. > > Yes, this looks good and also trivial. @coleenp, @dholmes-ora and @sspitsyn - thanks for the reviews! I suppose there isn't any way to give @robehn credit for his reviews when this fix was part of https://github.com/openjdk/jdk/pull/13519. ------------- PR Comment: https://git.openjdk.org/jdk/pull/13704#issuecomment-1532107167