src/Pure/Tools/server.scala
changeset 68904 09151c54aaac
parent 68903 58525b08eed1
child 68957 eef4e983fd9d
--- a/src/Pure/Tools/server.scala	Tue Sep 04 14:40:31 2018 +0200
+++ b/src/Pure/Tools/server.scala	Tue Sep 04 14:47:50 2018 +0200
@@ -276,7 +276,7 @@
     override def nodes_status(nodes_status: Document_Status.Nodes_Status)
     {
       val json =
-        for ((name, node_status) <- nodes_status.dest)
+        for ((name, node_status) <- nodes_status.present)
           yield name.json + ("status" -> nodes_status(name).json)
       context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
     }