# HG changeset patch
# User wenzelm
# Date 1592672756 -7200
# Node ID 2108c0e7ce13c3a5d4da5be9e4275964e8f2a967
# Parent  9d98a39aa509b7185c5e4c35b959b2c2c02b822d
tuned output;

diff -r 9d98a39aa509 -r 2108c0e7ce13 src/Pure/Admin/build_release.scala
--- 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) =>