# HG changeset patch
# User wenzelm
# Date 1476468187 -7200
# Node ID 1306a0e7fe81d04b7f1ae7cc5cec57cc4dec3b09
# Parent 6299566d00bc6179799bffcd95ac2dde88b65b41
explicit website directory;
diff -r 6299566d00bc -r 1306a0e7fe81 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala Fri Oct 14 19:49:38 2016 +0200
+++ b/src/Pure/Admin/build_release.scala Fri Oct 14 20:03:07 2016 +0200
@@ -20,6 +20,7 @@
official_release: Boolean = false,
release_name: String = "",
platform_families: List[String] = default_platform_families,
+ website: Option[Path] = None,
build_library: Boolean = false,
parallel_jobs: Int = 1,
remote_mac: String = ""): Release_Info =
@@ -94,15 +95,19 @@
/* minimal website */
- val existing_platform_bundles =
- Library.distinct(
- for {
- (a, b) <- main_platform_bundles ::: fallback_platform_bundles
- p = release_info.dist_dir + Path.explode(b)
- if p.is_file
- } yield (a, b), (x: (String, String), y: (String, String)) => x._1 == y._1)
+ website.foreach(dir =>
+ {
+ val website_platform_bundles =
+ Library.distinct(
+ for {
+ (a, b) <- main_platform_bundles ::: fallback_platform_bundles
+ p = release_info.dist_dir + Path.explode(b)
+ if p.is_file
+ } yield (a, b), (x: (String, String), y: (String, String)) => x._1 == y._1)
- File.write(release_info.dist_dir + Path.explode("index.html"),
+ Isabelle_System.mkdirs(dir)
+
+ File.write(dir + Path.explode("index.html"),
"""
@@ -113,7 +118,7 @@
""" + HTML.output(release_info.name) + """
""" +
- cat_lines(existing_platform_bundles.map({ case (a, b) =>
+ cat_lines(website_platform_bundles.map({ case (a, b) =>
"- " + HTML.output(b) + "
" })) +
"""
@@ -121,6 +126,9 @@
""")
+ for ((_, b) <- website_platform_bundles)
+ File.copy(release_info.dist_dir + Path.explode(b), dir)
+ })
/* HTML library */
@@ -151,6 +159,7 @@
var remote_mac = ""
var official_release = false
var release_name = ""
+ var website: Option[Path] = None
var parallel_jobs = 1
var build_library = false
var platform_families = default_platform_families
@@ -163,6 +172,7 @@
-M USER@HOST remote Mac OS X for dmg build
-O official release (not release-candidate)
-R RELEASE proper release with name
+ -W WEBSITE produce minimal website in given directory
-j INT maximum number of parallel jobs (default 1)
-l build library
-p NAMES platform families (comma separated list, default: """ +
@@ -174,6 +184,7 @@
"M:" -> (arg => remote_mac = arg),
"O" -> (_ => official_release = true),
"R:" -> (arg => release_name = arg),
+ "W:" -> (arg => website = Some(Path.explode(arg))),
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
"l" -> (_ => build_library),
"p:" -> (arg => platform_families = Library.space_explode(',', arg)),
@@ -185,7 +196,7 @@
val progress = new Console_Progress()
build_release(Path.explode(base_dir), progress = progress, rev = rev,
- official_release = official_release, release_name = release_name,
+ official_release = official_release, release_name = release_name, website = website,
platform_families =
if (platform_families.isEmpty) default_platform_families else platform_families,
build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac)