Please review a small fix to the documentation for the java.rmi module.
No webrev; here is the patch to remove an unnecessary line:
$ hg diff -R jdk
diff -r 13119f57b8da src/java.rmi/share/classes/module-info.java
--- a/src/java.rmi/share/classes/module-info.java Mon Jul 24 10:18:33
2017 -0400
+++ b/src/java.rmi/share/classes/module-info.java Mon Jul 24 13:37:15
2017 -0700
@@ -31,7 +31,6 @@
* object registry, and the <em>{@index rmid rmid tool}</em> tool to start
* the activation system daemon.
*
- * <p>
* <dl style="font-family:'DejaVu Sans', Arial, Helvetica, sans serif">
* <dt class="simpleTagLabel">Tool Guides:</dt>
* <dd> {@extLink rmiregistry_tool_reference rmiregistry},
JBS: https://bugs.openjdk.java.net/browse/JDK-8184217
-- Jon
