src/Pure/General/file_watcher.scala
changeset 71359 411c0322c09d
parent 64867 e7220f4de11f
child 71685 d5773922358d
--- 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 =