# HG changeset patch
# User wenzelm
# Date 1610716261 -3600
# Node ID 479668d61cef847dfc8d4e26cc2217828a27e3e9
# Parent  ff6b5e468d5f790a3484fea4a9ebee7a253b7e00
tuned;

diff -r ff6b5e468d5f -r 479668d61cef src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Jan 14 20:47:09 2021 +0100
+++ b/src/Pure/Tools/server.scala	Fri Jan 15 14:11:01 2021 +0100
@@ -272,7 +272,7 @@
     {
       val json =
         for ((name, node_status) <- nodes_status.present)
-          yield name.json + ("status" -> nodes_status(name).json)
+          yield name.json + ("status" -> node_status.json)
       context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
     }