# HG changeset patch
# User wenzelm
# Date 1615574629 -3600
# Node ID 043b56d882d30c08338240aac97a2efc0aa0b923
# Parent  7411d71b9fb80c002e9c9b8a00e0d7f2a887ff8b
tuned;

diff -r 7411d71b9fb8 -r 043b56d882d3 src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Fri Mar 12 19:42:18 2021 +0100
+++ b/src/Pure/Admin/components.scala	Fri Mar 12 19:43:49 2021 +0100
@@ -67,8 +67,7 @@
       val archive = base_dir + Path.explode(archive_name)
       if (!archive.is_file) {
         val remote = Components.default_component_repository + "/" + archive_name
-        progress.echo("Getting " + remote)
-        Bytes.write(archive, Url.read_bytes(Url(remote)))
+        Isabelle_System.download(remote, archive, progress = progress)
       }
       for (dir <- copy_dir) {
         Isabelle_System.make_directory(dir)
diff -r 7411d71b9fb8 -r 043b56d882d3 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Fri Mar 12 19:42:18 2021 +0100
+++ b/src/Pure/Tools/phabricator.scala	Fri Mar 12 19:43:49 2021 +0100
@@ -218,7 +218,7 @@
       val archive =
         if (Url.is_wellformed(mercurial_source)) {
           val archive = tmp_dir + Path.basic("mercurial.tar.gz")
-          Bytes.write(archive, Url.read_bytes(Url(mercurial_source)))
+          Isabelle_System.download(mercurial_source, archive)
           archive
         }
         else Path.explode(mercurial_source)