tuned output;
authorwenzelm
Sat, 20 Jun 2020 19:05:56 +0200
changeset 71973 2108c0e7ce13
parent 71972 9d98a39aa509
child 71974 e5fe4d40326d
tuned output;
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) =>