tuned signature;
authorwenzelm
Tue, 24 Jan 2023 11:34:39 +0100
changeset 77067 9ca1e7fc2663
parent 77066 72d87e32b062
child 77068 ef1831744f00
tuned signature;
src/Pure/Admin/build_release.scala
src/Pure/System/components.scala
--- a/src/Pure/Admin/build_release.scala	Tue Jan 24 11:30:56 2023 +0100
+++ b/src/Pure/Admin/build_release.scala	Tue Jan 24 11:34:39 2023 +0100
@@ -565,10 +565,12 @@
         val (bundled_components, jdk_component) =
           get_bundled_components(isabelle_target, platform)
 
-        Components.resolve(context.components_base, bundled_components,
-          target_dir = Some(contrib_dir),
-          copy_dir = Some(context.dist_dir + Path.explode("contrib")),
-          progress = progress)
+        for (name <- bundled_components) {
+          Components.resolve(context.components_base, name,
+            target_dir = Some(contrib_dir),
+            copy_dir = Some(context.dist_dir + Path.explode("contrib")),
+            progress = progress)
+        }
 
         val more_components_names =
           more_components.map(Components.unpack(contrib_dir, _, progress = progress))
--- a/src/Pure/System/components.scala	Tue Jan 24 11:30:56 2023 +0100
+++ b/src/Pure/System/components.scala	Tue Jan 24 11:34:39 2023 +0100
@@ -65,7 +65,7 @@
 
   def resolve(
     base_dir: Path,
-    names: List[String],
+    name: String,
     target_dir: Option[Path] = None,
     copy_dir: Option[Path] = None,
     component_repository: String = Components.default_component_repository,
@@ -73,19 +73,17 @@
     progress: Progress = new Progress
   ): Unit = {
     ssh.make_directory(base_dir)
-    for (name <- names) {
-      val archive_name = Archive(name)
-      val archive = base_dir + Path.explode(archive_name)
-      if (!ssh.is_file(archive)) {
-        val remote = Url.append_path(component_repository, archive_name)
-        ssh.download_file(remote, archive, progress = progress)
-      }
-      for (dir <- copy_dir) {
-        ssh.make_directory(dir)
-        ssh.copy_file(archive, dir)
-      }
-      unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress)
+    val archive_name = Archive(name)
+    val archive = base_dir + Path.explode(archive_name)
+    if (!ssh.is_file(archive)) {
+      val remote = Url.append_path(component_repository, archive_name)
+      ssh.download_file(remote, archive, progress = progress)
     }
+    for (dir <- copy_dir) {
+      ssh.make_directory(dir)
+      ssh.copy_file(archive, dir)
+    }
+    unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress)
   }
 
   private val platforms_family: Map[Platform.Family.Value, Set[String]] =