clarified defaults: explicit "rev" takes precedence;
authorwenzelm
Thu, 06 Dec 2018 16:40:56 +0100
changeset 69414 eab0d3108b46
parent 69413 52727566c1ba
child 69415 99c3529c31d0
clarified defaults: explicit "rev" takes precedence;
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Thu Dec 06 15:44:31 2018 +0100
+++ b/src/Pure/Admin/build_release.scala	Thu Dec 06 16:40:56 2018 +0100
@@ -252,7 +252,7 @@
       val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
       val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute
 
-      val version = proper_release_name orElse proper_string(rev) getOrElse "tip"
+      val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
       val ident =
         try { hg.id(version) }
         catch { case ERROR(_) => error("Bad repository version: " + version) }