diff -r 22c59d1ea818 -r 4990220334dc ViewManager/ViewManager.py
--- a/ViewManager/ViewManager.py Thu Jun 23 19:17:46 2016 +0200
+++ b/ViewManager/ViewManager.py Sun Jun 26 21:29:18 2016 +0200
@@ -4578,8 +4578,9 @@
@param fn filename of editor to update (string)
@param line line number to highlight (int)
"""
- self.openSourceFile(fn, line)
- self.setFileLine(fn, line)
+ if not fn.startswith('<'):
+ self.openSourceFile(fn, line)
+ self.setFileLine(fn, line)
def setFileLine(self, fn, line, error=False, syntaxError=False):
"""
