# HG changeset patch
# User wenzelm
# Date 1612875785 -3600
# Node ID 27dc8f8991478b5c3dc4cb9d9ce7b3b477ac3858
# Parent  180ecdf83bc8bdad17cb7b1fc184c6ccd1054bf2
clarified signature;

diff -r 180ecdf83bc8 -r 27dc8f899147 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Mon Feb 08 23:14:56 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Feb 09 14:03:05 2021 +0100
@@ -92,6 +92,9 @@
 
   /* integrity test of build_history vs. build_history_base */
 
+  def build_history_options0: String =
+    " -C '$USER_HOME/.isabelle/contrib' -f "
+
   val build_history_base: Logger_Task =
     Logger_Task("build_history_base", logger =>
       {
@@ -104,7 +107,7 @@
                 isabelle_identifier = "cronjob_build_history",
                 self_update = true,
                 rev = "build_history_base",
-                options = "-C '$USER_HOME/.isabelle/contrib' -f",
+                options = build_history_options0,
                 args = "HOL")
 
             for ((log_name, bytes) <- results) {
@@ -222,6 +225,14 @@
         pick_days(2000, 1)
       })
     }
+
+    def build_history_options: String =
+      " -h " + Bash.string(host) + " " +
+      (java_heap match {
+        case "" => ""
+        case h =>
+          "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + h + "\"' "
+      }) + options
   }
 
   val remote_builds_old: List[Remote_Build] =
@@ -415,14 +426,8 @@
                 rev = rev,
                 afp_rev = afp_rev,
                 options =
-                  " -C '$USER_HOME/.isabelle/contrib'" +
                   " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
-                  " -f -h " + Bash.string(r.host) + " " +
-                  (r.java_heap match {
-                    case "" => ""
-                    case h =>
-                      "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + h + "\"' "
-                  }) + r.options,
+                  build_history_options0 + r.build_history_options,
                 args = "-o timeout=10800 " + r.args)
 
             for ((log_name, bytes) <- results) {