src/Pure/Tools/build_cluster.scala
changeset 78584 92ef737f412c
parent 78582 63f06b935a1f
child 78592 fdfe9b91d96e
child 78638 28a2c55648d5
equal deleted inserted replaced
78583:8f11794211ef 78584:92ef737f412c
   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