# HG changeset patch
# User wenzelm
# Date 1674501828 -3600
# Node ID e233054dcb00562b2205ba3027e6ff34acb02945
# Parent  f60dd8d765159b19fefca84fc2d84ef9ba9d7ae7
clarified defaults;
proper Url.append_path;

diff -r f60dd8d76515 -r e233054dcb00 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Mon Jan 23 16:29:29 2023 +0100
+++ b/src/Pure/System/components.scala	Mon Jan 23 20:23:48 2023 +0100
@@ -58,6 +58,7 @@
   def resolve(base_dir: Path, names: List[String],
     target_dir: Option[Path] = None,
     copy_dir: Option[Path] = None,
+    component_repository: String = Components.default_component_repository,
     progress: Progress = new Progress
   ): Unit = {
     Isabelle_System.make_directory(base_dir)
@@ -65,7 +66,7 @@
       val archive_name = Archive(name)
       val archive = base_dir + Path.explode(archive_name)
       if (!archive.is_file) {
-        val remote = Components.default_component_repository + "/" + archive_name
+        val remote = Url.append_path(component_repository, archive_name)
         Isabelle_System.download_file(remote, archive, progress = progress)
       }
       for (dir <- copy_dir) {