# HG changeset patch # User wenzelm # Date 1476464893 -7200 # Node ID cb98e0e5f1e58f6df7c47401c2101413f86ed9ff # Parent bee9d2609404714eee7da1eb0696d492cd937da3 website index for existing bundles; diff -r bee9d2609404 -r cb98e0e5f1e5 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Fri Oct 14 17:35:10 2016 +0200 +++ b/src/Pure/Admin/build_release.scala Fri Oct 14 19:08:13 2016 +0200 @@ -92,6 +92,13 @@ /* minimal website */ + val existing_platform_bundles = + for { + (a, b) <- all_platform_bundles + p = release_info.dist_dir + Path.explode(b) + if p.is_file + } yield (a, b) + File.write(release_info.dist_dir + Path.explode("index.html"), """ @@ -103,7 +110,7 @@

""" + HTML.output(release_info.name) + """