tuned signature;
authorwenzelm
Sat, 17 Dec 2022 11:25:19 +0100
changeset 76662 762406d791f4
parent 76661 0c7c6fa71ac3
child 76663 b7546c25e4f0
tuned signature;
src/Pure/Admin/build_scala.scala
src/Tools/jEdit/src/jedit_resources.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 */
--- 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)))
       }