ViewManager/ViewManager.py

branch
6_1_x
changeset 5010
4990220334dc
parent 4898
87f323577ce1
--- 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):
         """

eric ide

mercurial