author | wenzelm |
Thu, 05 Jan 2017 16:23:51 +0100 | |
changeset 64803 | 27328dcaf64c |
parent 64802 | adc4c84b692c |
child 64804 | b2b05fdff3a7 |
--- a/src/Pure/PIDE/session.scala Thu Jan 05 16:16:18 2017 +0100 +++ b/src/Pure/PIDE/session.scala Thu Jan 05 16:23:51 2017 +0100 @@ -297,6 +297,7 @@ assignment |= assign for (command <- cmds) { nodes += command.node_name + command.blobs_names.foreach(nodes += _) commands += command } delay_flush.invoke()