changeset 64722 | 6df73de0d3c7 |
parent 64721 | 4b9c96c3850b |
child 64726 | c534a2ac537d |
--- a/src/Tools/VSCode/src/vscode_resources.scala Sat Dec 31 14:27:07 2016 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Dec 31 14:29:16 2016 +0100 @@ -89,7 +89,7 @@ (Some(model), st.copy(models = st.models + (uri -> model.copy(external = true)))) }) - def sync_external(changed_files: Set[JFile]): Boolean = + def sync_models(changed_files: Set[JFile]): Boolean = state.change_result(st => { val changed_models =