diff --git a/services/web/frontend/js/ide/editor/EditorManager.js b/services/web/frontend/js/ide/editor/EditorManager.js index ab8eb8913c..c9047c3876 100644 --- a/services/web/frontend/js/ide/editor/EditorManager.js +++ b/services/web/frontend/js/ide/editor/EditorManager.js @@ -75,6 +75,15 @@ define([ this.$scope.$on('flush-changes', () => { return Document.flushAll() }) + window.addEventListener('blur', () => { + // The browser may put the tab into sleep as it looses focus. + // Flushing the documents should help with keeping the documents in + // sync: we can use any new version of the doc that the server may + // present us. There should be no need to insert local changes into + // the doc history as the user comes back. + sl_console.log('[EditorManager] forcing flush onblur') + Document.flushAll() + }) this.$scope.$watch('editor.wantTrackChanges', value => { if (value == null) {