equal
deleted
inserted
replaced
146 } |
146 } |
147 |
147 |
148 def init(): Unit = remote_isabelle.init() |
148 def init(): Unit = remote_isabelle.init() |
149 |
149 |
150 def start(): Process_Result = { |
150 def start(): Process_Result = { |
|
151 val remote_ml_platform = remote_isabelle.getenv("ML_PLATFORM") |
|
152 if (remote_ml_platform != build_context.ml_platform) { |
|
153 error("Bad ML_PLATFORM: found " + remote_ml_platform + |
|
154 ", but expected " + build_context.ml_platform) |
|
155 } |
151 val script = |
156 val script = |
152 Build.build_worker_command(host, |
157 Build.build_worker_command(host, |
153 ssh = ssh, |
158 ssh = ssh, |
154 build_options = List(options.spec("build_database_server")), |
159 build_options = List(options.spec("build_database_server")), |
155 build_id = build_context.build_uuid, |
160 build_id = build_context.build_uuid, |