# 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] =