author | wenzelm |
Fri, 15 Jan 2021 14:11:01 +0100 | |
changeset 73132 | 479668d61cef |
parent 73131 | ff6b5e468d5f |
child 73133 | 497e11537d48 |
--- 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)) }