retain copy of required components;
authorwenzelm
Wed, 10 Apr 2019 13:43:23 +0200
changeset 70102 e48ffba6b557
parent 70101 4ae335fd3a54
child 70103 a6236d5a89ae
retain copy of required components;
src/Pure/Admin/build_release.scala
src/Pure/Admin/components.scala
--- a/src/Pure/Admin/build_release.scala	Wed Apr 10 12:38:27 2019 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Apr 10 13:43:23 2019 +0200
@@ -453,7 +453,9 @@
           get_bundled_components(isabelle_target, platform)
 
         Components.resolve(components_base, bundled_components,
-          target_dir = Some(contrib_dir), progress = progress)
+          target_dir = Some(contrib_dir),
+          copy_dir = Some(release.dist_dir + Path.explode("contrib")),
+          progress = progress)
 
         val more_components_names =
           more_components.map(Components.unpack(contrib_dir, _, progress = progress))
--- 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)
     }
   }