diff -r 556528860c7a -r 31a1eb0f70e4 ViewManager/ViewManager.py
--- a/ViewManager/ViewManager.py Thu Jun 23 19:24:09 2016 +0200
+++ b/ViewManager/ViewManager.py Sun Jun 26 21:29:18 2016 +0200
@@ -4577,8 +4577,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):
"""
