From 9e4c766edf539d0bb700433cc829d9ef3d8fc24c Mon Sep 17 00:00:00 2001
From: Michael Ernst <mernst@cs.washington.edu>
Date: Mon, 21 Mar 2022 11:36:42 -0700
Subject: [PATCH] Improve Maven instructions.  Fixes #5086.

---
 docs/manual/external-tools.tex | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/docs/manual/external-tools.tex b/docs/manual/external-tools.tex
index 9fa859534e4..e3674e8a0c6 100644
--- a/docs/manual/external-tools.tex
+++ b/docs/manual/external-tools.tex
@@ -973,8 +973,10 @@
   </dependencies>
 \end{alltt}
 
-Java 11 and later do not need the \<com.google.errorprone.javac>
+Java 11 and later do not need the \<com.google.errorprone:javac>
 dependency.  If you will never use Java 8, you can omit it.
+The need for the \<com.google.errorprone:javac> artifact when running under
+JDK 8 is explained in Section~\ref{javac-jdk8}.
 
 Periodically update to the most recent version, to obtain the
 latest bug fixes and new features:
@@ -982,9 +984,6 @@
   mvn versions:use-latest-versions -Dincludes="org.checkerframework:*"
 \end{Verbatim}
 
-The need for the \<com.google.errorprone:javac> artifact when running under
-JDK 8 is explained in Section~\ref{javac-jdk8}.
-
 \end{enumerate}
 
 \item If using JDK 8, use a Maven property to hold the location of the
@@ -1022,7 +1021,7 @@
   creating three new profiles as shown below (the example uses the Nullness
   Checker).  If your POM file does not already use the
   \code{maven-compiler-plugin} plugin, you are done.  If your POM file
-  already uses the plugin, copy edit the first profile to incorporate the
+  already uses the plugin, copy and edit the first profile to incorporate the
   existing configuration.
 
 %% TODO: Is this comment still accurate?
@@ -1145,7 +1144,7 @@
 \end{mysmall}
 
 Now, building with Maven will run the checkers during every compilation
-that uses JDK 8 or JDK 11.
+that uses JDK 8 or higher.
 
 If you wish to run checkers while compiling your source code but not your
 tests, wrap the \code{<configuration>...</configuration>} within
@@ -1160,8 +1159,10 @@
 \end{Verbatim}
 
 To compile without using the Checker Framework, pass
-\<-P '!checkerframework-java11'> (or \<-P '!checkerframework-java8'>)
+\<-P '!checkerframework>
 on the Maven command line.
+It should also work to pass
+\<-P '!checkerframework-jdk9orlater' or \<-P '!checkerframework-java8'>.
 
 % TODO: Figure out why, and then remove this paragraph.
 Warning:  adding