# HG changeset patch # User wenzelm # Date 1545576028 -3600 # Node ID 4c1985eba1b780bb7deba232d2e17be41e85a305 # Parent db001bc11855842a75116a9683cf57b239418103 tuned message; diff -r db001bc11855 -r 4c1985eba1b7 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Sat Dec 22 17:02:29 2018 +0100 +++ b/src/Pure/Admin/build_release.scala Sun Dec 23 15:40:28 2018 +0100 @@ -619,9 +619,11 @@ // executable archive (self-extracting 7z) - val exe_archive = tmp_dir + Path.explode(isabelle_name + ".7z") + val archive_name = isabelle_name + ".7z" + val exe_archive = tmp_dir + Path.explode(archive_name) exe_archive.file.delete + progress.echo("Packaging " + archive_name + " ...") execute(tmp_dir, "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name)) if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)