# HG changeset patch
# User wenzelm
# Date 1639390758 -3600
# Node ID 9a2958ec9e088c5c3ac05c4a93167d78132679fb
# Parent  115a47a103aa30bc468b0bb51c75a0865c4e29d5
updated links;

diff -r 115a47a103aa -r 9a2958ec9e08 src/Doc/JEdit/JEdit.thy
--- 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.
diff -r 115a47a103aa -r 9a2958ec9e08 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sat Dec 11 13:06:46 2021 +0100
+++ b/src/Doc/System/Server.thy	Mon Dec 13 11:19:18 2021 +0100
@@ -493,7 +493,7 @@
 
   \<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
   as plain text.\<^footnote>\<open>See \<^url>\<open>https://www.ietf.org/rfc/rfc4122.txt\<close> and
-  \<^url>\<open>https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/util/UUID.html\<close>.\<close> Such
+  \<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/UUID.html\<close>.\<close> Such
   identifiers are created as private random numbers of the server and only
   revealed to the client that creates a certain resource (e.g.\ task or
   session). A client may disclose this information for use in a different