On Tue, 17 Nov 2020 20:56:52 GMT, Jim Laskey <jlaskey at openjdk.org> wrote: > my local branch seems to have the right sources for doc Maybe, but your branch on GitHub does not. ------------- PR: https://git.openjdk.java.net/jdk/pull/1273