src/Pure/General/file_watcher.scala
changeset 73359 d8a0e996614b
parent 73353 279e45248e9d
child 73367 77ef8bef0593
--- a/src/Pure/General/file_watcher.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/file_watcher.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -105,7 +105,7 @@
                         key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala
                       val remove = if (key.reset) None else Some(dir)
                       val changed =
-                        (Set.empty[JFile] /: events.iterator) {
+                        events.iterator.foldLeft(Set.empty[JFile]) {
                           case (set, event) => set + dir.toPath.resolve(event.context).toFile
                         }
                       (remove, changed)