--- a/src/Doc/JEdit/JEdit.thy Sat Dec 11 13:06:46 2021 +0100
+++ b/src/Doc/JEdit/JEdit.thy Mon Dec 13 11:19:18 2021 +0100
@@ -1154,7 +1154,7 @@
\<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some
regular expression, in the notation that is commonly used on the Java
- platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
+ platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
This may serve as an additional visual filter of the result.
\<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.