--- a/Admin/etc/options Tue Sep 29 20:00:59 2020 +0200
+++ b/Admin/etc/options Tue Sep 29 20:08:08 2020 +0200
@@ -12,11 +12,11 @@
-- "unpacked components for remote build services"
-option build_release_server_linux : string = ""
+option build_host_linux : string = ""
-- "SSH user@host for remote build of heaps"
-option build_release_server_macos : string = ""
+option build_host_macos : string = ""
-- "SSH user@host for remote build of heaps"
-option build_release_server_windows : string = ""
+option build_host_windows : string = ""
-- "SSH user@host for remote build of heaps"
--- a/src/Pure/Admin/build_release.scala Tue Sep 29 20:00:59 2020 +0200
+++ b/src/Pure/Admin/build_release.scala Tue Sep 29 20:08:08 2020 +0200
@@ -228,7 +228,7 @@
build_sessions: List[String],
local_dir: Path)
{
- val server_option = "build_release_server_" + platform.toString
+ val server_option = "build_host_" + platform.toString
options.string(server_option) match {
case SSH.Target(user, host) =>
using(SSH.open_session(options, host = host, user = user))(ssh =>