equal
deleted
inserted
replaced
294 } |
294 } |
295 |
295 |
296 val remote_builds1: List[List[Remote_Build]] = { |
296 val remote_builds1: List[List[Remote_Build]] = { |
297 List( |
297 List( |
298 List(Remote_Build("Linux (ARM)", "server-arm", |
298 List(Remote_Build("Linux (ARM)", "server-arm", |
|
299 history_base = "build_history_base_arm", |
299 options = "-m32 -B -M1x2" + |
300 options = "-m32 -B -M1x2" + |
300 " -e ISABELLE_SWIPL=swipl")), |
301 " -e ISABELLE_SWIPL=swipl")), |
301 List(Remote_Build("Linux B", "lxbroy10", history = 90, |
302 List(Remote_Build("Linux B", "lxbroy10", history = 90, |
302 options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), |
303 options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), |
303 List( |
304 List( |