# HG changeset patch # User wenzelm # Date 1510664198 -3600 # Node ID 85e6c1ff5be3027db38dddea097049c74f23993c # Parent f11486d3158630349ae9ef9b6e6221f4dabb2c58 removed pointless user_home: no measurable impact; diff -r f11486d31586 -r 85e6c1ff5be3 src/Pure/Admin/isabelle_cronjob.scala --- 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",