ViewManager/ViewManager.py

branch
5_4_x
changeset 3262
fffe2df45766
parent 3160
209a07d7e401
child 3323
b55fcd897118
--- a/ViewManager/ViewManager.py	Sat Feb 01 18:41:02 2014 +0100
+++ b/ViewManager/ViewManager.py	Sat Feb 08 20:09:58 2014 +0100
@@ -4543,7 +4543,8 @@
         filenames = []
         for editor in self.editors:
             fn = editor.getFileName()
-            if fn is not None and fn not in filenames:
+            if fn is not None and fn not in filenames and os.path.exists(fn):
+                # only return names of existing files
                 filenames.append(fn)
         
         return filenames

eric ide

mercurial