# HG changeset patch
# User wenzelm
# Date 1488736697 -3600
# Node ID 31fd8e41be02367a20d041d3e7653c5ec873b2a2
# Parent  29c19bc97d201a1979ce51838d9f36df9e4ba576
tuned signature;

diff -r 29c19bc97d20 -r 31fd8e41be02 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)