# HG changeset patch
# User wenzelm
# Date 1663839012 -7200
# Node ID 544e81a2c9fc5125720828779a06783c8ccd3674
# Parent  19978abbc1116e35d7df56871037971f7e007229
tuned signature: removed unused operations;

diff -r 19978abbc111 -r 544e81a2c9fc src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Sep 22 11:21:45 2022 +0200
+++ b/src/Pure/Tools/build.scala	Thu Sep 22 11:30:12 2022 +0200
@@ -138,11 +138,9 @@
 
   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) {
     def sessions: Set[String] = results.keySet
-    def infos: List[Sessions.Info] = results.values.map(_._2).toList
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
+    def info(name: String): Sessions.Info = results(name)._2
     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
-    def get_info(name: String): Option[Sessions.Info] = results.get(name).map(_._2)
-    def info(name: String): Sessions.Info = get_info(name).get
     val rc: Int =
       results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
         foldLeft(Process_Result.RC.ok)(_ max _)