author | wenzelm |
Sun, 05 Mar 2017 18:58:17 +0100 | |
changeset 65118 | 31fd8e41be02 |
parent 65117 | 29c19bc97d20 |
child 65119 | a7bedf94e71c |
--- a/src/Tools/VSCode/src/vscode_resources.scala Sun Mar 05 14:47:37 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Mar 05 18:58:17 2017 +0100 @@ -220,7 +220,7 @@ /* pending output */ - def update_output(changed_nodes: List[JFile]): Unit = + def update_output(changed_nodes: Traversable[JFile]): Unit = state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes)) def flush_output(channel: Channel)