tuned signature;
authorwenzelm
Sun, 05 Mar 2017 18:58:17 +0100
changeset 65118 31fd8e41be02
parent 65117 29c19bc97d20
child 65119 a7bedf94e71c
tuned signature;
src/Tools/VSCode/src/vscode_resources.scala
--- 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)