On Wed, 11 Nov 2020 11:56:57 GMT, Aleksey Shipilev <sh...@openjdk.org> wrote:
>> Right! Fixed that. > > Well, and `make update-build-docs` made no changes after this, so I guess > pandoc did not care. Maybe it is missing indents... Yes, indents were incorrect. Fixed, and now generated html looks fine. ------------- PR: https://git.openjdk.java.net/jdk/pull/1160
