# HG changeset patch
# User wenzelm
# Date 1477159076 -7200
# Node ID 4c253e84ae6266fa24249cacbe33b82db716f69f
# Parent  602483aa7818cf532a33ce62170511888c266fc4
clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);

diff -r 602483aa7818 -r 4c253e84ae62 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Oct 22 19:14:38 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Oct 22 19:57:56 2016 +0200
@@ -373,6 +373,7 @@
     isabelle_repos_other: Path,
     isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
     self_update: Boolean = false,
+    push_isabelle_home: Boolean = false,
     progress: Progress = Ignore_Progress,
     progress_result: (String, Bytes) => Unit = (log_name: String, bytes: Bytes) => (),
     options: String = "",
@@ -387,13 +388,24 @@
       Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = Some(ssh))
 
     if (self_update) {
-      isabelle_hg.pull()
-      isabelle_hg.update(clean = true)
+      if (push_isabelle_home) {
+        val isabelle_home_hg = Mercurial.repository(Path.explode("~~"))
+        val rev = isabelle_home_hg.id()
+        isabelle_home_hg.push(isabelle_hg.root_url, rev = rev, force = true)
+        isabelle_hg.update(rev = rev, clean = true)
+      }
+      else {
+        isabelle_hg.pull()
+        isabelle_hg.update(clean = true)
+      }
       ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
     }
 
-    Mercurial.setup_repository(
-      ssh.bash_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
+    val other_hg =
+      Mercurial.setup_repository(
+        ssh.bash_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
+    other_hg.pull(isabelle_hg.root.implode)
+    other_hg.update(rev = isabelle_hg.id(), clean = true)
 
 
     /* Admin/build_history */
diff -r 602483aa7818 -r 4c253e84ae62 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 22 19:14:38 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 22 19:57:56 2016 +0200
@@ -117,6 +117,9 @@
         using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))(
           ssh =>
             {
+              val self_update = !r.shared_home
+              val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
+
               def progress_result(log_name: String, bytes: Bytes): Unit =
                 Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
 
@@ -124,7 +127,8 @@
                 isabelle_repos,
                 isabelle_repos.ext(r.host),
                 isabelle_repos_source = isabelle_dev_source,
-                self_update = !r.shared_home,
+                self_update = self_update,
+                push_isabelle_home = push_isabelle_home,
                 progress_result = progress_result _,
                 options =
                   r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name),
diff -r 602483aa7818 -r 4c253e84ae62 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Oct 22 19:14:38 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Oct 22 19:57:56 2016 +0200
@@ -106,6 +106,12 @@
     def log(rev: String = "", template: String = "", options: String = ""): String =
       hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
 
+    def push(remote: String = "", rev: String = "", force: Boolean = false, options: String = "")
+    {
+      hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
+        check
+    }
+
     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
       hg.command("pull", opt_rev(rev) + optional(remote), options).check