--- a/src/Pure/Admin/isabelle_cronjob.scala Mon Nov 13 15:07:03 2017 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Tue Nov 14 13:56:38 2017 +0100
@@ -264,7 +264,7 @@
detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
private def remote_build_history(
- rev: String, afp_rev: Option[String], i: Int, user_home: Boolean, r: Remote_Build): Logger_Task =
+ rev: String, afp_rev: Option[String], i: Int, r: Remote_Build): Logger_Task =
{
val task_name = "build_history-" + r.host
Logger_Task(task_name, logger =>
@@ -275,14 +275,6 @@
val self_update = !r.shared_home
val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
- if (user_home && r.shared_home) {
- ssh.execute("""
-if [ ! -e /tmp/isabelle-isatest/contrib ]
-then
- mkdir -p /tmp/isabelle-isatest && ln -s /home/isabelle/contrib /tmp/isabelle-isatest
-fi""").check
- }
-
val results =
Build_History.remote_build_history(ssh,
isabelle_repos,
@@ -293,7 +285,6 @@
rev = rev,
afp_rev = afp_rev,
options =
- (if (user_home && r.shared_home) " -u /tmp/isabelle-isatest" else "") +
" -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
" -f " + r.options,
args = "-o timeout=10800 " + r.args)
@@ -448,9 +439,6 @@
val hg = Mercurial.repository(isabelle_repos)
val hg_graph = hg.graph()
- val user_home: String => Boolean =
- hg_graph.all_succs(List("19b6091c2137")).contains(_)
-
def history_base_filter(r: Remote_Build): Item => Boolean =
{
val base_rev = hg.id(r.history_base)
@@ -475,7 +463,7 @@
for {
(r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
(rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
- } yield remote_build_history(rev, afp_rev, i, user_home(rev), r)))),
+ } yield remote_build_history(rev, afp_rev, i, r)))),
Logger_Task("jenkins_logs", _ =>
Jenkins.download_logs(Jenkins.build_log_jobs, main_dir)),
Logger_Task("build_log_database",