# HG changeset patch
# User wenzelm
# Date 1554892707 -7200
# Node ID 4ae335fd3a54c309788021e80a722f19ce4b37f3
# Parent  d9ea307aac2aae5c764acb9bc18417150e8673fd
option for build_sessions;

diff -r d9ea307aac2a -r 4ae335fd3a54 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Apr 10 12:11:30 2019 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Apr 10 12:38:27 2019 +0200
@@ -222,10 +222,13 @@
 
   /* build heaps on remote server */
 
-  def remote_build_heaps(
-    options: Options, family: Platform.Family.Value, local_dir: Path, build_sessions: List[String])
+  private def remote_build_heaps(
+    options: Options,
+    platform: Platform.Family.Value,
+    build_sessions: List[String],
+    local_dir: Path)
   {
-    val server_option = "build_release_server_" + family.toString
+    val server_option = "build_release_server_" + platform.toString
     options.string(server_option) match {
       case SSH.Target(user, host) =>
         using(SSH.open_session(options, host = host, user = user))(ssh =>
@@ -270,6 +273,7 @@
     platform_families: List[Platform.Family.Value] = default_platform_families,
     more_components: List[Path] = Nil,
     website: Option[Path] = None,
+    build_sessions: List[String] = Nil,
     build_library: Boolean = false,
     parallel_jobs: Int = 1): Release =
   {
@@ -488,6 +492,14 @@
         val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
 
 
+        // build heaps
+
+        if (build_sessions.nonEmpty) {
+          progress.echo("Building " + commas(build_sessions) + " ...")
+          remote_build_heaps(options, platform, build_sessions, isabelle_target)
+        }
+
+
         // application bundling
 
         platform match {
@@ -748,6 +760,7 @@
       var official_release = false
       var proper_release_name: Option[String] = None
       var website: Option[Path] = None
+      var build_sessions: List[String] = Nil
       var more_components: List[Path] = Nil
       var parallel_jobs = 1
       var build_library = false
@@ -765,6 +778,7 @@
     -O           official release (not release-candidate)
     -R RELEASE   proper release with name
     -W WEBSITE   produce minimal website in given directory
+    -b SESSIONS  build platform-specific session images (separated by commas)
     -c ARCHIVE   clean bundling with additional component .tar.gz archive
     -j INT       maximum number of parallel jobs (default 1)
     -l           build library
@@ -779,6 +793,7 @@
         "O" -> (_ => official_release = true),
         "R:" -> (arg => proper_release_name = Some(arg)),
         "W:" -> (arg => website = Some(Path.explode(arg))),
+        "b:" -> (arg => build_sessions = space_explode(',', arg)),
         "c:" -> (arg =>
           {
             val path = Path.explode(arg)
@@ -805,8 +820,8 @@
         platform_families =
           if (platform_families.isEmpty) default_platform_families
           else platform_families,
-        more_components = more_components, build_library = build_library,
-        parallel_jobs = parallel_jobs)
+        more_components = more_components, build_sessions = build_sessions,
+        build_library = build_library, parallel_jobs = parallel_jobs)
     }
   }
 }