tuned --- rename = dist_name is sufficient;
authorwenzelm
Wed, 05 May 2021 20:41:40 +0200
changeset 73888 7c70f10e0b3b
parent 73887 f17caa5002df
child 73889 7e465e166bb2
tuned --- rename = dist_name is sufficient;
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed May 05 20:37:49 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed May 05 20:41:40 2021 +0200
@@ -916,7 +916,7 @@
         }
         else {
           val archive = Release_Archive.get(source_archive, rename = release_name)
-          val context = make_context(proper_string(release_name) getOrElse archive.identifier)
+          val context = make_context(archive.identifier)
           Isabelle_System.new_directory(context.dist_dir)
           use_release_archive(context, archive, id = rev)
           context