# HG changeset patch # User wenzelm # Date 1677767954 -3600 # Node ID abc9706a4ca2da8ef04b8f0468ea146a10870854 # Parent e50cad69cbe79ede0d50ed1020a8fcfb9b615aed tuned; diff -r e50cad69cbe7 -r abc9706a4ca2 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Thu Mar 02 15:04:24 2023 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Mar 02 15:39:14 2023 +0100 @@ -196,11 +196,9 @@ 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 + if_proper(java_heap, + "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + java_heap + "\"' ") + + options } val remote_builds_old: List[Remote_Build] =