update the file tree selection whenever a document is opened GitOrigin-RevId: 88d7b651b43d0a0ca5fa9998d4c42c7b1d3effc5
@@ -146,6 +146,8 @@ define([
}
if (doc.id === this.$scope.editor.open_doc_id && !options.forceReopen) {
+ // automatically update the file tree whenever the file is opened
+ this.ide.fileTreeManager.selectEntity(doc)
this.$scope.$apply(() => {
return done()
})
@@ -1018,8 +1018,6 @@ define([
ide.editorManager.openDoc(entity, {
gotoLine: line,
gotoColumn: column
- // commented out because it causes an out of sync error
- // forceReopen: true