# HG changeset patch
# User wenzelm
# Date 1674556575 -3600
# Node ID ef1831744f00e8879a69a7331af39d30bd4697dc
# Parent  9ca1e7fc2663e1b9d1583d5606ca5f0b011918d9
more strict;

diff -r 9ca1e7fc2663 -r ef1831744f00 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Tue Jan 24 11:34:39 2023 +0100
+++ b/src/Pure/System/components.scala	Tue Jan 24 11:36:15 2023 +0100
@@ -74,7 +74,7 @@
   ): Unit = {
     ssh.make_directory(base_dir)
     val archive_name = Archive(name)
-    val archive = base_dir + Path.explode(archive_name)
+    val archive = base_dir + Path.basic(archive_name)
     if (!ssh.is_file(archive)) {
       val remote = Url.append_path(component_repository, archive_name)
       ssh.download_file(remote, archive, progress = progress)