author | wenzelm |
Sat, 20 Jun 2020 19:05:56 +0200 | |
changeset 71973 | 2108c0e7ce13 |
parent 71972 | 9d98a39aa509 |
child 71974 | e5fe4d40326d |
--- a/src/Pure/Admin/build_release.scala Sat Jun 20 16:36:32 2020 +0200 +++ b/src/Pure/Admin/build_release.scala Sat Jun 20 19:05:56 2020 +0200 @@ -720,7 +720,7 @@ HTML.write_document(dir, "index.html", List(HTML.title(release.dist_name)), List( - HTML.section(release.dist_name + " (" + release.ident + ")"), + HTML.section(release.dist_name), HTML.subsection("Platforms"), HTML.itemize( website_platform_bundles.map({ case (bundle, bundle_info) =>