# HG changeset patch
# User wenzelm
# Date 1544110856 -3600
# Node ID eab0d3108b46fd55f423ed78e929396e409c0307
# Parent  52727566c1ba768cab1f2bf33e1482ee866f2a39
clarified defaults: explicit "rev" takes precedence;

diff -r 52727566c1ba -r eab0d3108b46 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) }