# HG changeset patch
# User wenzelm
# Date 1477218077 -7200
# Node ID 8f628de5108bb6c14b7cdc2adbb90d14d0695859
# Parent  74ece0e491b650384abe57b45d20e0a94b517fbe
more explicit rev (tip);

diff -r 74ece0e491b6 -r 8f628de5108b src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sun Oct 23 11:38:43 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Sun Oct 23 12:21:17 2016 +0200
@@ -387,25 +387,30 @@
     val isabelle_hg =
       Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = Some(ssh))
 
-    if (self_update) {
-      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)
+    val rev =
+      if (self_update) {
+        val rev =
+          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)
+            rev
+          }
+          else {
+            isabelle_hg.pull()
+            isabelle_hg.id()
+          }
         isabelle_hg.update(rev = rev, clean = true)
+        ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
+        rev
       }
-      else {
-        isabelle_hg.pull()
-        isabelle_hg.update(clean = true)
-      }
-      ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
-    }
+      else "tip"
 
     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)
+    other_hg.update(rev = rev, clean = true)
 
 
     /* Admin/build_history */