# HG changeset patch
# User wenzelm
# Date 1654005690 -7200
# Node ID ee51db628e711c438df6b86796730ef137a99fc8
# Parent  57e292106d713747ab2b9f243aa04b2fcc41914d
clarified signature;

diff -r 57e292106d71 -r ee51db628e71 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue May 31 13:29:47 2022 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue May 31 16:01:30 2022 +0200
@@ -551,7 +551,7 @@
         strict = strict).check
 
     if (self_update) {
-      val hg = Mercurial.repository(Path.ISABELLE_HOME)
+      val hg = Mercurial.self_repository()
       hg.push(self_hg.root_url, force = true)
       self_hg.update(rev = hg.parent(), clean = true)
 
diff -r 57e292106d71 -r ee51db628e71 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Tue May 31 13:29:47 2022 +0200
+++ b/src/Pure/Admin/build_release.scala	Tue May 31 16:01:30 2022 +0200
@@ -398,7 +398,7 @@
   ): Unit = {
     val progress = context.progress
 
-    val hg = Mercurial.repository(Path.ISABELLE_HOME)
+    val hg = Mercurial.self_repository()
     val id =
       try { hg.id(version) }
       catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
diff -r 57e292106d71 -r ee51db628e71 src/Pure/Admin/sync_repos.scala
--- a/src/Pure/Admin/sync_repos.scala	Tue May 31 13:29:47 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala	Tue May 31 16:01:30 2022 +0200
@@ -22,7 +22,7 @@
   ): Unit = {
     val target_dir = if (target.endsWith(":") || target.endsWith("/")) target else target + "/"
 
-    val isabelle_hg = Mercurial.repository(Path.ISABELLE_HOME)
+    val hg = Mercurial.self_repository()
     val afp_hg = afp_root.map(Mercurial.repository(_))
 
     val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil
@@ -32,12 +32,12 @@
         thorough = thorough, dry_run = dry_run, clean = clean, filter = filter ::: more_filter)
 
     progress.echo("\n* Isabelle repository:")
-    sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect /etc/ISABELLE_ID"))
+    sync(hg, target, rev, filter = List("protect /AFP", "protect /etc/ISABELLE_ID"))
 
     if (!dry_run) {
       Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
         val id_path = tmp_dir + Path.explode("ISABELLE_ID")
-        File.write(id_path, isabelle_hg.id(rev = rev))
+        File.write(id_path, hg.id(rev = rev))
         Isabelle_System.rsync(port = port, thorough = thorough,
           args = List(File.standard_path(id_path), target_dir + "etc/"))
       }
diff -r 57e292106d71 -r ee51db628e71 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue May 31 13:29:47 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Tue May 31 16:01:30 2022 +0200
@@ -127,6 +127,8 @@
     hg
   }
 
+  def self_repository(): Repository = repository(Path.ISABELLE_HOME)
+
   def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = {
     @tailrec def find(root: Path): Option[Repository] =
       if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))