# HG changeset patch
# User wenzelm
# Date 1476529674 -7200
# Node ID 407f69c4959f572cd84877e649d019f3eb742a9e
# Parent e7cbf81ec4b7fc5bafc8380daf07f304252c7b5a
identify release;
diff -r e7cbf81ec4b7 -r 407f69c4959f Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist Sat Oct 15 11:38:03 2016 +0200
+++ b/Admin/lib/Tools/makedist Sat Oct 15 13:07:54 2016 +0200
@@ -118,6 +118,8 @@
DIR="$DISTBASE/$DISTNAME"
[ -e "$DIR" ] && fail "Directory \"$DIR\" already exists"
+rm -f "$DISTPREFIX/ISABELLE_DIST" "$DISTPREFIX/ISABELLE_IDENT"
+
# retrieve repository archive
@@ -212,8 +214,8 @@
cd "$DISTBASE"
-echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
-echo "$IDENT" >../ISABELLE_IDENT
+echo "$DISTBASE/$DISTNAME.tar.gz" > "$DISTPREFIX/ISABELLE_DIST"
+echo "$IDENT" > "$DISTPREFIX/ISABELLE_IDENT"
chown -R "$LOGNAME" "$DISTNAME"
chmod -R g=o "$DISTNAME"
diff -r e7cbf81ec4b7 -r 407f69c4959f src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala Sat Oct 15 11:38:03 2016 +0200
+++ b/src/Pure/Admin/build_release.scala Sat Oct 15 13:07:54 2016 +0200
@@ -10,7 +10,8 @@
object Build_Release
{
sealed case class Release_Info(
- date: Date, name: String, dist_dir: Path, dist_archive: Path, dist_library_archive: Path)
+ date: Date, name: String, dist_dir: Path, dist_archive: Path, dist_library_archive: Path,
+ id: String)
private val default_platform_families = List("linux", "windows", "windows64", "macos")
@@ -34,7 +35,7 @@
val dist_dir = base_dir + Path.explode("dist-" + name)
val dist_archive = dist_dir + Path.explode(name + ".tar.gz")
val dist_library_archive = dist_dir + Path.explode(name + "_library.tar.gz")
- Release_Info(date, name, dist_dir, dist_archive, dist_library_archive)
+ Release_Info(date, name, dist_dir, dist_archive, dist_library_archive, "")
}
val main_platform_bundles =
@@ -59,16 +60,27 @@
val jobs_option = " -j" + parallel_jobs.toString
- if (release_info.dist_archive.is_file)
- progress.echo("### Release archive already exists: " + release_info.dist_archive.implode)
- else {
- progress.echo("Producing release archive " + release_info.dist_archive.implode + " ...")
- progress.bash(
- "isabelle makedist -d " + File.bash_path(base_dir) + jobs_option +
- (if (official_release) " -O" else "") +
- (if (release_name != "") " -r " + File.bash_string(release_name) else "") +
- (if (rev != "") " " + File.bash_string(rev) else ""),
- echo = true).check
+ val release_id =
+ {
+ val isabelle_ident_file = base_dir + Path.explode("ISABELLE_IDENT")
+ val isabelle_dist_file = base_dir + Path.explode("ISABELLE_DIST")
+
+ if (release_info.dist_archive.is_file &&
+ isabelle_ident_file.is_file && isabelle_dist_file.is_file &&
+ File.eq(Path.explode(Library.trim_line(File.read(isabelle_dist_file))),
+ release_info.dist_archive)) {
+ progress.echo("### Release archive already exists: " + release_info.dist_archive.implode)
+ }
+ else {
+ progress.echo("Producing release archive " + release_info.dist_archive.implode + " ...")
+ progress.bash(
+ "isabelle makedist -d " + File.bash_path(base_dir) + jobs_option +
+ (if (official_release) " -O" else "") +
+ (if (release_name != "") " -r " + File.bash_string(release_name) else "") +
+ (if (rev != "") " " + File.bash_string(rev) else ""),
+ echo = true).check
+ }
+ Library.trim_line(File.read(isabelle_ident_file))
}
@@ -115,7 +127,7 @@
-""" + HTML.output(release_info.name) + """
+""" + HTML.output(release_info.name + " (" + release_id + ")") + """
""" +
cat_lines(website_platform_bundles.map({ case (a, b) =>
@@ -146,7 +158,7 @@
}
- release_info
+ release_info.copy(id = release_id)
}