tuned messages;
authorwenzelm
Mon, 22 Oct 2018 11:48:28 +0200
changeset 69176 63391630495f
parent 69175 561dc80624db
child 69177 300046d2ec60
tuned messages;
src/Pure/Admin/build_release.scala
--- 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")