ensure records can be used with java 15 as well GitOrigin-RevId: 5716dddb35ad9b2349e6558460897d650740fe1c