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