# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737112612 -3600
# Node ID 8abdf3b0074b9a75b503d2b62aca78073e70a76b
# Parent  11c3f6d4e7e694254e7585f3867d99fa38cc5ac6
clarified: sync_id operation, similar to archive_id;

diff -r 11c3f6d4e7e6 -r 8abdf3b0074b 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