Note about Error Prone javac dependency (#5744)

Author: mernst

docs/manual/external-tools.tex

@@ -1010,7 +1010,7 @@
 \end{alltt}
 
 Java 11 and later do not need the \<com.google.errorprone:javac>
-dependency.
+dependency, but it does no harm.
 The need for the \<com.google.errorprone:javac> artifact when running under
 JDK 8 is explained in Section~\ref{javac-jdk8}.