# 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)