# HG changeset patch
# User wenzelm
# Date 1601402888 -7200
# Node ID 0973a594be72e2177ee38515343c512f81c331f8
# Parent  676066aa47982b2529210e787a57f69d095d4806
clarified names;

diff -r 676066aa4798 -r 0973a594be72 Admin/etc/options
--- 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"
diff -r 676066aa4798 -r 0973a594be72 src/Pure/Admin/build_release.scala
--- 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 =>