# HG changeset patch # User wenzelm # Date 1674556479 -3600 # Node ID 9ca1e7fc2663e1b9d1583d5606ca5f0b011918d9 # Parent 72d87e32b0629fdcb2eb09b17dc8458f018d7cc8 tuned signature; diff -r 72d87e32b062 -r 9ca1e7fc2663 src/Pure/Admin/build_release.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)) diff -r 72d87e32b062 -r 9ca1e7fc2663 src/Pure/System/components.scala --- 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]] =