On Fri, 3 Nov 2023 17:30:00 GMT, Pavel Rappo <pra...@openjdk.org> wrote:
> Please review this PR to fix an internal error caused by (malfunctioning > diagnostics for) spurious markup in hybrid and external snippets. > > Spurious markup resembles snippet markup, but isn't one. In particular, > spurious markup has no effect on snippet processing and, if appears in the > displayed region, is shown as is. Marked as reviewed by jjg (Reviewer). ------------- PR Review: https://git.openjdk.org/jdk/pull/16501#pullrequestreview-1725134682
