changeset 68888 | 4fe165254e20 |
parent 68884 | 9b97d0b20d95 |
child 68894 | 1dbdad1b57a5 |
--- a/src/Pure/Thy/thy_resources.scala Sun Sep 02 23:08:31 2018 +0200 +++ b/src/Pure/Thy/thy_resources.scala Sun Sep 02 23:25:53 2018 +0200 @@ -153,7 +153,7 @@ val delay_nodes_status = Standard_Thread.delay_first(nodes_status_delay max Time.zero) { val (nodes_status, names) = nodes_status_update.value - progress.nodes_status(names.map(name => (name -> nodes_status(name)))) + progress.nodes_status(nodes_status, names) } val consumer =