On Tue, 22 Nov 2022 20:57:45 GMT, Christoph Langer <[email protected]> wrote:
>> So this PR is good as is? > >> @RealCLanger yes, you're good to go. >> >> The next step is for you to enter `/integrate` as a comment. > > Thanks, @jonathan-gibbons, for approving. Technically I know what to do to > get this merged. I just wasn't sure whether you were ok with the fix or > suggesting something different. So... > > @RealCLanger yes, you're good to go. > > The next step is for you to enter `/integrate` as a comment. > > Thanks, @jonathan-gibbons, for approving. Technically I know what to do to > get this merged. I just wasn't sure whether you were ok with the fix or > suggesting something different. So... > > /integrate Yeah, I was just commenting on the possible approaches to an issue like this. ------------- PR: https://git.openjdk.org/jdk/pull/11177
