On Tue, 17 Nov 2020 21:10:48 GMT, Kevin Rushforth <k...@openjdk.org> wrote:
>> @erikj79 my local branch seems to have the right sources for doc > >> my local branch seems to have the right sources for doc > > Maybe, but your branch on GitHub does not. @kevinrushforth What is the recommended approach to remove the doc edit/commit? ------------- PR: https://git.openjdk.java.net/jdk/pull/1273