clarified self_update: imitate visible directory state on remote side;
authorwenzelm
Sat, 03 Mar 2018 15:09:36 +0100
changeset 67756 d2fe32ebe3c7
parent 67755 208235e594f6
child 67757 f6f77517dc32
clarified self_update: imitate visible directory state on remote side;
src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Mar 03 14:54:56 2018 +0100
+++ b/src/Pure/Admin/build_history.scala	Sat Mar 03 15:09:36 2018 +0100
@@ -529,9 +529,8 @@
 
     if (self_update) {
       val hg = Mercurial.repository(Path.explode("~~"))
-      val self_rev = hg.id()
-      hg.push(self_hg.root_url, rev = self_rev, force = true)
-      self_hg.update(rev = self_rev, clean = true)
+      hg.push(self_hg.root_url, force = true)
+      self_hg.update(rev = hg.parent(), clean = true)
 
       execute("bin/isabelle", "components -I")
       execute("bin/isabelle", "components -a", echo = true)