# 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)) }