changeset 64782 | 3f0bbb60859b |
parent 64710 | 72ca4e5f976e |
child 64807 | 7d556bb6046b |
--- a/src/Pure/General/file_watcher.scala Wed Jan 04 21:29:19 2017 +0100 +++ b/src/Pure/General/file_watcher.scala Wed Jan 04 22:31:40 2017 +0100 @@ -45,6 +45,12 @@ st.copy(dirs = st.dirs + (dir -> key)) }) + def register_parent(file: JFile): Unit = + { + val dir = file.getParentFile + if (dir != null && dir.isDirectory) register(dir) + } + def deregister(dir: JFile): Unit = state.change(st => st.dirs.get(dir) match {