Stop spinner on PDF sync when file does not exist anymore GitOrigin-RevId: cba4bf3dd3d90c2894c6c5f1b28d184f18bb08fd
@@ -68,3 +68,6 @@ modules/**/Makefile
# via dev-environment
.npmrc
+
+# Intellij
+.idea
@@ -1063,7 +1063,7 @@ App.factory('synctex', function(ide, $http, $q) {
) {
const doc = ide.fileTreeManager.findEntityByPath(data.code[0].file)
if (doc == null) {
- return
+ deferred.reject()
}
return deferred.resolve({ doc, line: data.code[0].line })
} else if (data.code[0].file === '') {