proper dist_name;
authorwenzelm
Wed, 05 May 2021 20:37:49 +0200
changeset 73887 f17caa5002df
parent 73886 f2e836e013cb
child 73888 7c70f10e0b3b
proper dist_name;
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed May 05 14:17:25 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed May 05 20:37:49 2021 +0200
@@ -509,7 +509,7 @@
       Bytes.write(archive_path, archive.bytes)
       val extract =
         List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
-          map(name => context.release_name + "/" + name)
+          map(name => context.dist_name + "/" + name)
       execute_tar(context.dist_dir,
         "-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract))
     })