# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1710939535 -3600
# Node ID f08e5a234c1bcfcb1772720e828f8f92908d7419
# Parent  7bac6bd83cc31a25ae0fc56e349bf32d9f8e437f
always check if node is defined, e.g. for exists_next operation wit empty schedule;

diff -r 7bac6bd83cc3 -r f08e5a234c1b src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Tue Mar 19 13:24:22 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Wed Mar 20 13:58:55 2024 +0100
@@ -576,6 +576,7 @@
       val next_nodes =
         for {
           task <- state.next_ready
+          if graph.defined(task.name)
           node = graph.get_node(task.name)
           if hostname == node.node_info.hostname
         } yield node