equal
deleted
inserted
replaced
170 build_options = List(options.spec("build_database_server")), |
170 build_options = List(options.spec("build_database_server")), |
171 build_id = build_context.build_uuid, |
171 build_id = build_context.build_uuid, |
172 isabelle_home = remote_isabelle_home, |
172 isabelle_home = remote_isabelle_home, |
173 afp_root = remote_afp_root, |
173 afp_root = remote_afp_root, |
174 dirs = Path.split(host.dirs).map(remote_isabelle.expand_path)) |
174 dirs = Path.split(host.dirs).map(remote_isabelle.expand_path)) |
175 remote_isabelle.bash(script).print.check |
175 remote_isabelle.bash(script).check |
176 } |
176 } |
177 |
177 |
178 override def close(): Unit = ssh.close() |
178 override def close(): Unit = ssh.close() |
179 } |
179 } |
180 |
180 |