git: openjdk/jdk16: 8258338: Support deprecated records

[Jonathan Gibbons]

Changeset: ce0ab2dd
Author:    Jonathan Gibbons <jjg at openjdk.org>
Date:      2020-12-16 22:26:57 +0000
URL:       https://git.openjdk.java.net/jdk16/commit/ce0ab2dd

8258338: Support deprecated records

Reviewed-by: hannesw

! src/jdk.javadoc/share/classes/jdk/javadoc/internal/doclets/formats/html/DeprecatedListWriter.java
! src/jdk.javadoc/share/classes/jdk/javadoc/internal/doclets/formats/html/resources/standard.properties
! src/jdk.javadoc/share/classes/jdk/javadoc/internal/doclets/toolkit/resources/doclets.properties
! src/jdk.javadoc/share/classes/jdk/javadoc/internal/doclets/toolkit/util/DeprecatedAPIListBuilder.java
! test/langtools/jdk/javadoc/doclet/testRecordTypes/TestRecordTypes.java