# HG changeset patch
# User wenzelm
# Date 1617227116 -7200
# Node ID 419edc7f372685fe7d421e8c7dccb2141dc69617
# Parent  c52d819499a1ec7db9937a99b0f9b3139b2f69ef
clarified signature;

diff -r c52d819499a1 -r 419edc7f3726 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Mar 31 23:13:13 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Mar 31 23:45:16 2021 +0200
@@ -404,7 +404,6 @@
             execute_tar(tmp_dir, "-xzf " +
               File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
             Isabelle_System.isabelle_id(root = tmp_dir + release.isabelle)
-              .getOrElse(error("Failed to determine ISABELLE_ID from " + release.isabelle_archive))
           })
 
       if (release.ident != archive_ident) {
diff -r c52d819499a1 -r 419edc7f3726 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Mar 31 23:13:13 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Mar 31 23:45:16 2021 +0200
@@ -189,16 +189,16 @@
 
   /* Isabelle distribution identification */
 
-  def isabelle_id(root: Path = Path.ISABELLE_HOME): Option[String] =
-    getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) orElse {
-      if (Mercurial.is_repository(root)) Some(Mercurial.repository(root).parent())
-      else None
+  def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
+    getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse {
+      if (Mercurial.is_repository(root)) Mercurial.repository(root).parent()
+      else error("Failed to identify Isabelle distribution " + root)
     }
 
   object Isabelle_Id extends Scala.Fun("isabelle_id")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = isabelle_id().get
+    def apply(arg: String): String = isabelle_id()
   }
 
   def isabelle_tags(root: Path = Path.ISABELLE_HOME): String =