author | Fabian Huch <huch@in.tum.de> |
Fri, 17 Jan 2025 12:16:52 +0100 | |
changeset 81821 | 8abdf3b0074b |
parent 81820 | 11c3f6d4e7e6 |
child 81822 | e7be7c4b871c |
--- 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