# HG changeset patch
# User wenzelm
# Date 1671272719 -3600
# Node ID 762406d791f46f789e86dfa8978fe5a91c2762ed
# Parent  0c7c6fa71ac3e32b164e4c07591f174ee1139faa
tuned signature;

diff -r 0c7c6fa71ac3 -r 762406d791f4 src/Pure/Admin/build_scala.scala
--- a/src/Pure/Admin/build_scala.scala	Sat Dec 17 11:25:10 2022 +0100
+++ b/src/Pure/Admin/build_scala.scala	Sat Dec 17 11:25:19 2022 +0100
@@ -78,7 +78,7 @@
       download.get(component_dir.lib + Path.basic(download.artifact), progress = progress))
 
     File.write(component_dir.LICENSE,
-      Url.read(Url("https://www.apache.org/licenses/LICENSE-2.0.txt")))
+      Url.read("https://www.apache.org/licenses/LICENSE-2.0.txt"))
 
 
     /* classpath */
diff -r 0c7c6fa71ac3 -r 762406d791f4 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Sat Dec 17 11:25:10 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Sat Dec 17 11:25:19 2022 +0100
@@ -74,7 +74,7 @@
       val name = node_name.node
       try {
         val text =
-          if (Url.is_wellformed(name)) Url.read(Url(name))
+          if (Url.is_wellformed(name)) Url.read(name)
           else File.read(new JFile(name))
         Some(Symbol.decode(Line.normalize(text)))
       }