src/Pure/Tools/build.scala

--- a/src/Pure/Tools/build.scala	Wed Oct 18 19:53:39 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Oct 18 20:07:54 2023 +0200
@@ -114,9 +114,6 @@
       else options1 + "build_database_server" + "build_database"
     }
 
-    def process_options(options: Options, node_info: Host.Node_Info): Options =
-      Host.node_options(options, node_info)
-
     final def build_store(options: Options,
       build_hosts: List[Build_Cluster.Host] = Nil,
       cache: Term.Cache = Term.Cache.make()