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)