Merge "Make 'make docs' work on OpenJDK 9 toolchain."