--- a/make/jdk/src/classes/build/tools/jdwpgen/RootNode.java Mon Jul 22 14:40:00 2019 +0200
+++ b/make/jdk/src/classes/build/tools/jdwpgen/RootNode.java Mon Jul 22 10:26:21 2019 -0700
@@ -53,7 +53,7 @@
writer.println("</head>");
writer.println("<body>");
writer.println("<div class=\"centered\" role=\"banner\">");
- writer.println("<h1 id=\"Protocol Details\">Java Debug Wire Protocol Details</h1>");
+ writer.println("<h1 id=\"Protocol_Details\">Java Debug Wire Protocol Details</h1>");
writer.println("</div>");
writer.println("<nav>");
writer.println("<ul>");