clarified names;
authorwenzelm
Tue, 29 Sep 2020 20:08:08 +0200
changeset 72341 0973a594be72
parent 72340 676066aa4798
child 72342 4195e75a92ef
clarified names;
Admin/etc/options
src/Pure/Admin/build_release.scala
--- 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 =>