Changeset: 0bf678dd8951 Author: jjg Date: 2019-07-12 10:44 -0700 URL: https://hg.openjdk.java.net/jdk/jdk/rev/0bf678dd8951 8227613: "draft" header should be in a <header> instead of <div> Reviewed-by: mchung, iris ! make/Docs.gmk