src/Pure/Admin/components.scala
changeset 70102 e48ffba6b557
parent 69703 1e30b4093924
child 71601 97ccf48c2f0c
--- a/src/Pure/Admin/components.scala	Wed Apr 10 12:38:27 2019 +0200
+++ b/src/Pure/Admin/components.scala	Wed Apr 10 13:43:23 2019 +0200
@@ -55,6 +55,7 @@
 
   def resolve(base_dir: Path, names: List[String],
     target_dir: Option[Path] = None,
+    copy_dir: Option[Path] = None,
     progress: Progress = No_Progress)
   {
     Isabelle_System.mkdirs(base_dir)
@@ -66,6 +67,10 @@
         progress.echo("Getting " + remote)
         Bytes.write(archive, Url.read_bytes(Url(remote)))
       }
+      for (dir <- copy_dir) {
+        Isabelle_System.mkdirs(dir)
+        File.copy(archive, dir)
+      }
       unpack(target_dir getOrElse base_dir, archive, progress = progress)
     }
   }