# HG changeset patch
# User wenzelm
# Date 1417440245 -3600
# Node ID 27c6936c6484c667f71bd9b4a37a6a5f6d83d411
# Parent  4af6060734d51e6f88318b947fb1c8b8e3a18eb9
tuned signature;

diff -r 4af6060734d5 -r 27c6936c6484 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Dec 01 13:49:47 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Dec 01 14:24:05 2014 +0100
@@ -27,8 +27,8 @@
   {
     type Entry = (Long, XML.Tree)
     val empty = new Results(SortedMap.empty)
-    def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _)
-    def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _)
+    def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
+    def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
   }
 
   final class Results private(private val rep: SortedMap[Long, XML.Tree])