init user settings on fresh test machine;
authorwenzelm
Mon, 16 Oct 2017 11:37:14 +0200
changeset 66871 a804fa68f62c
parent 66870 f801b36d7c4e
child 66872 69afe45a6062
init user settings on fresh test machine;
src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Mon Oct 16 08:00:28 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Mon Oct 16 11:37:14 2017 +0200
@@ -495,9 +495,10 @@
           isabelle_hg.id()
         }
       isabelle_hg.update(rev = self_rev, clean = true)
-      ssh.execute(
-        ssh.bash_path(isabelle_repos_self + Path.explode("bin/isabelle"))
-          + " components -a").check
+      for (cmd <- List("components -I", "components -a")) {
+        ssh.execute(
+          ssh.bash_path(isabelle_repos_self + Path.explode("bin/isabelle")) + " " + cmd).check
+      }
       ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
     }