On Thu, 4 May 2023 18:01:10 GMT, Jonathan Gibbons <j...@openjdk.org> wrote:
> Please review a simple fix to remove unnecessary detail from in-page and > console messages about the name of the tag enclosing a bad reference. Looks good to me. ------------- Marked as reviewed by hannesw (Reviewer). PR Review: https://git.openjdk.org/jdk/pull/13811#pullrequestreview-1416594403
