--- 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]] =