changeset 64858 | e31cf6eaecb8 |
parent 64807 | 7d556bb6046b |
child 64859 | e600cfdc9e97 |
--- a/src/Pure/General/file_watcher.scala Mon Jan 09 21:51:39 2017 +0100 +++ b/src/Pure/General/file_watcher.scala Mon Jan 09 22:54:48 2017 +0100 @@ -25,9 +25,10 @@ object File_Watcher { + val none: File_Watcher = new File_Watcher + def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher = - if (Platform.is_windows) new File_Watcher - else new Impl(handle, delay) + if (Platform.is_windows) none else new Impl(handle, delay) /* proper implementation */