changeset 64722 | 6df73de0d3c7 |
parent 64720 | 8cc2d7c4ada1 |
child 64724 | 44dbf8cc2d7f |
--- a/src/Tools/VSCode/src/server.scala Sat Dec 31 14:27:07 2016 +0100 +++ b/src/Tools/VSCode/src/server.scala Sat Dec 31 14:29:16 2016 +0100 @@ -127,7 +127,7 @@ } private def sync_external(changed: Set[JFile]): Unit = - if (resources.sync_external(changed)) delay_input.invoke() + if (resources.sync_models(changed)) delay_input.invoke() private val watcher = File_Watcher(sync_external(_))