ViewManager/ViewManager.py

branch
debugger speed
changeset 5006
82e91d2f59a1
parent 4917
682750cc7bd5
child 5108
f5cb9cb98e6a
diff -r 684f5ba04f0b -r 82e91d2f59a1 ViewManager/ViewManager.py
--- a/ViewManager/ViewManager.py	Sun Jun 26 16:32:01 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):
         """

eric ide

mercurial