# HG changeset patch # User wenzelm # Date 1528233975 -7200 # Node ID 54f07e7f68f94d4bcee76e370c93957bdde397e2 # Parent 4a3fc3420747c5233afae289fd3127f5aa74d103 more parallelism to cope with 8h30 CPU time; diff -r 4a3fc3420747 -r 54f07e7f68f9 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Tue Jun 05 21:29:54 2018 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Tue Jun 05 23:26:15 2018 +0200 @@ -260,7 +260,7 @@ List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), List(Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90, - options = "-m32 -B -M1,2 -t Benchmarks" + + options = "-m32 -B -M1x2,2 -t Benchmarks" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_SMLNJ=sml -e ISABELLE_SWIPL=swipl", args = "-N -a -d '~~/src/Benchmarks'",