--- 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)
--- 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) }
--- 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/"))
}
--- 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))