# HG changeset patch
# User wenzelm
# Date 1476387146 -7200
# Node ID 351b8211aef90e6f5780b2e05213fa13e2700487
# Parent  c43dedbb81181a3072ab2bd8b707387e9132a01e
tuned;

diff -r c43dedbb8118 -r 351b8211aef9 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 21:23:49 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 21:32:26 2016 +0200
@@ -28,18 +28,11 @@
 
   /* identify Isabelle + AFP repository snapshots */
 
-  private def pull_repos(root: Path): String =
-  {
-    val hg = Mercurial.repository(root)
-    hg.pull(options = "-q")
-    hg.identify("tip", options = "-i")
-  }
-
   private val isabelle_identify =
     Logger_Task("isabelle_identify", logger =>
       {
-        val isabelle_id = pull_repos(isabelle_repos)
-        val afp_id = pull_repos(afp_repos)
+        val isabelle_id = Mercurial.repository(isabelle_repos).pull_id()
+        val afp_id = Mercurial.repository(afp_repos).pull_id()
 
         File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
           terminate_lines(
diff -r c43dedbb8118 -r 351b8211aef9 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Thu Oct 13 21:23:49 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Thu Oct 13 21:32:26 2016 +0200
@@ -77,6 +77,12 @@
     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
       hg.command("pull", opt_rev(rev) + optional(remote), options).check
 
+    def pull_id(remote: String = ""): String =
+    {
+      hg.pull(remote = remote, options = "-q")
+      hg.identify("tip", options = "-i")
+    }
+
     def update(
       rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
     {