# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717484538 -7200
# Node ID b6551e0c70c4b9b4b4193de473503947cb4483b5
# Parent  885fc1e837eda0e905997d12e809f42b85d0fe8b
support ci job via hg_sync (cf. 7883f221d6d3);

diff -r 885fc1e837ed -r b6551e0c70c4 src/Pure/Admin/ci_build.scala
--- a/src/Pure/Admin/ci_build.scala	Mon Jun 03 19:37:42 2024 +0200
+++ b/src/Pure/Admin/ci_build.scala	Tue Jun 04 09:02:18 2024 +0200
@@ -133,7 +133,8 @@
   }
 
   def hg_id(path: Path): String =
-    Mercurial.repository(path).id()
+    if (Mercurial.Hg_Sync.ok(path)) File.read(path + Mercurial.Hg_Sync.PATH_ID)
+    else Mercurial.repository(path).id()
 
   def print_section(title: String): Unit =
     println("\n=== " + title + " ===\n")