--- 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(
--- 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 = "")
{