clarified: sync_id operation, similar to archive_id;
authorFabian Huch <huch@in.tum.de>
Fri, 17 Jan 2025 12:16:52 +0100
changeset 81821 8abdf3b0074b
parent 81820 11c3f6d4e7e6
child 81822 e7be7c4b871c
clarified: sync_id operation, similar to archive_id;
src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Thu Jan 16 16:10:26 2025 +0100
+++ b/src/Pure/General/mercurial.scala	Fri Jan 17 12:16:52 2025 +0100
@@ -117,6 +117,9 @@
 
   /* hg_sync meta data */
 
+  def sync_id(root: Path, ssh: SSH.System = SSH.Local): Option[String] =
+    if (Hg_Sync.ok(root, ssh)) Some(Hg_Sync.directory(root, ssh).id) else None
+
   object Hg_Sync {
     val NAME = ".hg_sync"
     val _NAME: String = " " + NAME