src/Pure/Tools/build_job.scala

--- a/src/Pure/Tools/build_job.scala	Tue Mar 14 10:35:41 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Tue Mar 14 11:14:50 2023 +0100
@@ -17,11 +17,6 @@
 }
 
 object Build_Job {
-  sealed case class Result(node_info: Host.Node_Info, process_result: Process_Result) {
-    def ok: Boolean = process_result.ok
-  }
-
-
   /* build session */
 
   def start_session(