--- a/src/Pure/Admin/build_release.scala Mon Oct 22 11:45:56 2018 +0200
+++ b/src/Pure/Admin/build_release.scala Mon Oct 22 11:48:28 2018 +0200
@@ -175,7 +175,7 @@
val version = proper_release_name orElse proper_string(rev) getOrElse "tip"
val ident =
try { hg.id(version) }
- catch { case ERROR(_) => error("Bad repository version: " + quote(version)) }
+ catch { case ERROR(_) => error("Bad repository version: " + version) }
val dist_version =
proper_release_name match {
@@ -217,7 +217,7 @@
error("Directory " + release.isabelle_dir + " already exists")
- progress.echo("### Retrieving Mercurial repository version " + quote(release.ident))
+ progress.echo("### Retrieving Mercurial repository version " + release.ident)
hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")