--- a/src/Pure/General/file_watcher.scala Thu Jan 09 13:44:16 2020 +0100
+++ b/src/Pure/General/file_watcher.scala Thu Jan 09 13:47:08 2020 +0100
@@ -12,7 +12,7 @@
import java.nio.file.{WatchKey, WatchEvent, Path => JPath}
import java.nio.file.StandardWatchEventKinds.{ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY}
-import scala.collection.JavaConversions
+import scala.collection.JavaConverters
class File_Watcher private[File_Watcher] // dummy template
@@ -102,7 +102,7 @@
st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
case Some(dir) =>
val events =
- JavaConversions.collectionAsScalaIterable(
+ JavaConverters.collectionAsScalaIterable(
key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
val remove = if (key.reset) None else Some(dir)
val changed =