# HG changeset patch
# User wenzelm
# Date 1446658550 -3600
# Node ID 320fa9d01e67d630743898b465d09b64ea5c3146
# Parent  ddb3ac3fef45b1d475ce28422241cfb5a651d8d5
updated;

diff -r ddb3ac3fef45 -r 320fa9d01e67 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Nov 04 18:32:47 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Wed Nov 04 18:35:50 2015 +0100
@@ -976,7 +976,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
-  "http://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html"}\<close>
+  "https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html"}\<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.